Theorem eluni 3917

Description: Membership in class union. (Contributed by NM, 22-May-1994.)

Assertion

Ref	Expression
eluni	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem eluni

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2825	. 2 |- ( A e. U. B -> A e. _V )
2		elex 2825	. . . 4 |- ( A e. x -> A e. _V )
3	2	adantr 276	. . 3 |- ( ( A e. x /\ x e. B ) -> A e. _V )
4	3	exlimiv 1647	. 2 |- ( E. x ( A e. x /\ x e. B ) -> A e. _V )
5		eleq1 2295	. . . . 5 |- ( y = A -> ( y e. x <-> A e. x ) )
6	5	anbi1d 465	. . . 4 |- ( y = A -> ( ( y e. x /\ x e. B ) <-> ( A e. x /\ x e. B ) ) )
7	6	exbidv 1874	. . 3 |- ( y = A -> ( E. x ( y e. x /\ x e. B ) <-> E. x ( A e. x /\ x e. B ) ) )
8		df-uni 3915	. . 3 |- U. B = { y | E. x ( y e. x /\ x e. B ) }
9	7, 8	elab2g 2964	. 2 |- ( A e. _V -> ( A e. U. B <-> E. x ( A e. x /\ x e. B ) ) )
10	1, 4, 9	pm5.21nii 712	1 |- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1398   E.wex 1541   e. wcel 2203   _Vcvv 2813   U.cuni 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-uni 3915

This theorem is referenced by:  eluni2  3918  elunii  3919  eluniab  3926  uniun  3933  uniin  3934  uniss  3935  unissb  3944  dftr2  4210  unidif0  4280  unipw  4333  uniex2  4557  uniuni  4572  limom  4736  dmuni  4966  fununi  5424  nfvres  5706  elunirn  5939  tfrlem7  6548  tfrexlem  6565  tfrcldm  6594  fiuni  7265  isbasis2g  14910  tgval2  14916  ntreq0  14997  bj-uniex2  16686