Theorem eluni2 4865

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 1861	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4864	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 303	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3440  df-uni 4862

This theorem is referenced by:  uni0b  4887  intssuni  4923  iuncom4  4953  inuni  5292  cnvuni  5833  chfnrn  6987  ssorduni  7719  unon  7770  limuni3  7792  frrlem9  8234  onfununi  8271  oarec  8487  uniinqs  8731  fissuni  9266  finsschain  9268  r1sdom  9689  rankuni2b  9768  cflm  10163  coflim  10174  axdc3lem2  10364  fpwwe2lem11  10554  uniwun  10653  tskr1om2  10681  tskuni  10696  axgroth3  10744  inaprc  10749  tskmval  10752  tskmcl  10754  suplem1pr  10965  lbsextlem2  21084  lbsextlem3  21085  isbasis3g  22852  eltg2b  22862  tgcl  22872  ppttop  22910  epttop  22912  neiptoptop  23034  tgcmp  23304  locfincmp  23429  dissnref  23431  comppfsc  23435  1stckgenlem  23456  txuni2  23468  txcmplem1  23544  tgqtop  23615  filuni  23788  alexsubALTlem4  23953  ptcmplem3  23957  ptcmplem4  23958  utoptop  24138  icccmplem1  24727  icccmplem3  24729  cnheibor  24870  bndth  24873  lebnumlem1  24876  bcthlem4  25243  ovolicc2lem5  25438  dyadmbllem  25516  itg2gt0  25677  rexunirn  32454  unipreima  32600  acunirnmpt2  32617  acunirnmpt2f  32618  elrspunidl  33378  ssdifidllem  33406  ssmxidllem  33423  reff  33808  locfinreflem  33809  cmpcref  33819  ddemeas  34205  dya2iocuni  34253  bnj1379  34799  cvmsss2  35249  cvmseu  35251  untuni  35684  dfon2lem3  35761  dfon2lem7  35765  dfon2lem8  35766  brbigcup  35874  neibastop1  36335  neibastop2lem  36336  fvineqsneq  37388  heicant  37637  mblfinlem1  37639  cover2  37697  heiborlem9  37801  unichnidl  38013  erimeq2  38658  prtlem16  38850  prter2  38862  prter3  38863  ssunib  43196  onsupuni  43205  onsuplub  43224  restuni3  45099  disjinfi  45173  cncfuni  45871  intsaluni  46314  salgencntex  46328