Theorem eluni2 4875

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 4874	. 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 4871

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 3449  df-uni 4872

This theorem is referenced by:  uni0b  4897  intssuni  4934  iuncom4  4964  inuni  5305  cnvuni  5850  chfnrn  7021  ssorduni  7755  unon  7806  limuni3  7828  frrlem9  8273  onfununi  8310  oarec  8526  uniinqs  8770  fissuni  9308  finsschain  9310  r1sdom  9727  rankuni2b  9806  cflm  10203  coflim  10214  axdc3lem2  10404  fpwwe2lem11  10594  uniwun  10693  tskr1om2  10721  tskuni  10736  axgroth3  10784  inaprc  10789  tskmval  10792  tskmcl  10794  suplem1pr  11005  lbsextlem2  21069  lbsextlem3  21070  isbasis3g  22836  eltg2b  22846  tgcl  22856  ppttop  22894  epttop  22896  neiptoptop  23018  tgcmp  23288  locfincmp  23413  dissnref  23415  comppfsc  23419  1stckgenlem  23440  txuni2  23452  txcmplem1  23528  tgqtop  23599  filuni  23772  alexsubALTlem4  23937  ptcmplem3  23941  ptcmplem4  23942  utoptop  24122  icccmplem1  24711  icccmplem3  24713  cnheibor  24854  bndth  24857  lebnumlem1  24860  bcthlem4  25227  ovolicc2lem5  25422  dyadmbllem  25500  itg2gt0  25661  rexunirn  32421  unipreima  32567  acunirnmpt2  32584  acunirnmpt2f  32585  elrspunidl  33399  ssdifidllem  33427  ssmxidllem  33444  reff  33829  locfinreflem  33830  cmpcref  33840  ddemeas  34226  dya2iocuni  34274  bnj1379  34820  cvmsss2  35261  cvmseu  35263  untuni  35696  dfon2lem3  35773  dfon2lem7  35777  dfon2lem8  35778  brbigcup  35886  neibastop1  36347  neibastop2lem  36348  fvineqsneq  37400  heicant  37649  mblfinlem1  37651  cover2  37709  heiborlem9  37813  unichnidl  38025  erimeq2  38670  prtlem16  38862  prter2  38874  prter3  38875  ssunib  43209  onsupuni  43218  onsuplub  43237  restuni3  45112  disjinfi  45186  cncfuni  45884  intsaluni  46327  salgencntex  46341