Theorem eluni2 4878

Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)

Assertion

Ref	Expression
eluni2	⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eluni2

Step	Hyp	Ref	Expression
1		exancom 1894	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4877	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3092	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 306	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091  ∪ cuni 4874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-v 3459  df-uni 4875

This theorem is used by:  uni0b  4901  intssuni  4937  iuncom4  4967  inuni  5322  cnvuni  5878  chfnrn  7048  ssorduni  7780  unon  7829  limuni3  7850  frrlem9  8293  onfununi  8330  oarec  8549  uniinqs  8797  fissuni  9317  finsschain  9319  r1sdom  9749  rankuni2b  9828  cflm  10244  coflim  10256  axdc3lem2  10446  fpwwe2lem11  10637  uniwun  10736  tskr1om2  10764  tskuni  10779  axgroth3  10827  inaprc  10832  tskmval  10835  tskmcl  10837  suplem1pr  11048  lbsextlem2  21312  lbsextlem3  21313  unichnlidl  21391  ssdifidllem  21513  isbasis3g  23135  eltg2b  23145  tgcl  23155  ppttop  23193  epttop  23195  neiptoptop  23317  tgcmp  23587  locfincmp  23712  dissnref  23714  comppfsc  23718  1stckgenlem  23739  txuni2  23751  txcmplem1  23827  tgqtop  23898  filuni  24071  alexsubALTlem4  24236  ptcmplem3  24240  ptcmplem4  24241  utoptop  24420  icccmplem1  25009  icccmplem3  25011  cnheibor  25143  bndth  25146  lebnumlem1  25149  bcthlem4  25515  ovolicc2lem5  25709  dyadmbllem  25787  itg2gt0  25948  rexunirn  32867  unipreima  33017  acunirnmpt2  33034  acunirnmpt2f  33035  elrspunidl  33759  ssmxidllem  33779  reff  34252  locfinreflem  34253  cmpcref  34263  ddemeas  34650  dya2iocuni  34697  bnj1379  35242  cvmsss2  35779  cvmseu  35781  untuni  36214  dfon2lem3  36288  dfon2lem7  36292  dfon2lem8  36293  brbigcup  36401  neibastop1  36903  neibastop2lem  36904  fvineqsneq  38091  heicant  38339  mblfinlem1  38341  cover2  38399  heiborlem9  38503  unichnidl  38715  erimeq2  39445  prtlem16  39676  prter2  39688  prter3  39689  ssunib  43980  onsupuni  43989  onsuplub  44008  restuni3  45869  disjinfi  45943  cncfuni  46633  intsaluni  47076  salgencntex  47090