Theorem eluni 3859

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 2785	. 2 |- ( A e. U. B -> A e. _V )
2		elex 2785	. . . 4 |- ( A e. x -> A e. _V )
3	2	adantr 276	. . 3 |- ( ( A e. x /\ x e. B ) -> A e. _V )
4	3	exlimiv 1622	. 2 |- ( E. x ( A e. x /\ x e. B ) -> A e. _V )
5		eleq1 2269	. . . . 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 1849	. . 3 |- ( y = A -> ( E. x ( y e. x /\ x e. B ) <-> E. x ( A e. x /\ x e. B ) ) )
8		df-uni 3857	. . 3 |- U. B = { y | E. x ( y e. x /\ x e. B ) }
9	7, 8	elab2g 2924	. 2 |- ( A e. _V -> ( A e. U. B <-> E. x ( A e. x /\ x e. B ) ) )
10	1, 4, 9	pm5.21nii 706	1 |- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   E.wex 1516   e. wcel 2177   _Vcvv 2773   U.cuni 3856

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-uni 3857

This theorem is referenced by:  eluni2  3860  elunii  3861  eluniab  3868  uniun  3875  uniin  3876  uniss  3877  unissb  3886  dftr2  4152  unidif0  4219  unipw  4269  uniex2  4491  uniuni  4506  limom  4670  dmuni  4897  fununi  5351  nfvres  5623  elunirn  5848  tfrlem7  6416  tfrexlem  6433  tfrcldm  6462  fiuni  7095  isbasis2g  14592  tgval2  14598  ntreq0  14679  bj-uniex2  15990