Theorem eluni2 2507

Description: Membership in class union. Restricted quantifier version.

Assertion

Ref	Expression
eluni2	|- (A e. U.B <-> E.x e. B A e. x)

Distinct variable groups:   x,A   x,B

Proof of Theorem eluni2

Step	Hyp	Ref	Expression
1		exancom 1054	. 2 |- (E.x(A e. x /\ x e. B) <-> E.x(x e. B /\ A e. x))
2		eluni 2506	. 2 |- (A e. U.B <-> E.x(A e. x /\ x e. B))
3		df-rex 1650	. 2 |- (E.x e. B A e. x <-> E.x(x e. B /\ A e. x))
4	1, 2, 3	3bitr4 183	1 |- (A e. U.B <-> E.x e. B A e. x)

Syntax hints:   <-> wb 146   /\ wa 223   e. wcel 958  E.wex 980  E.wrex 1646  U.cuni 2503

This theorem is referenced by:  uni0b 2523  intssuni 2555  iununi 2616  ssorduni 2993  unon 3088  limuni3 3123  reluni 3265  cnvuni 3301  chfnrn 3802  rankuni2 4690  cflim 4909  isbasis3g 7613  unitgt 7623  tgclt 7624  basgen2t 7639  bastop 7642  opnuni 7868  unirnbl 7875  axgroth3 8779  ntunte 10439

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rex 1650  df-v 1812  df-uni 2504

Copyright terms: Public domain