Theorem eluni2 4871

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 4870	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 306	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3086  ∪ cuni 4867

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-uni 4868

This theorem is used by:  uni0b  4894  intssuni  4930  iuncom4  4960  inuni  5314  cnvuni  5870  chfnrn  7041  ssorduni  7778  unon  7827  limuni3  7848  frrlem9  8293  onfununi  8330  oarec  8549  uniinqs  8797  fissuni  9324  finsschain  9326  r1sdom  9756  rankuni2b  9835  cflm  10251  coflim  10263  axdc3lem2  10453  fpwwe2lem11  10650  uniwun  10749  tskr1om2  10777  tskuni  10792  axgroth3  10840  inaprc  10845  tskmval  10848  tskmcl  10850  suplem1pr  11061  lbsextlem2  21346  lbsextlem3  21347  unichnlidl  21425  ssdifidllem  21547  isbasis3g  23174  eltg2b  23184  tgcl  23194  ppttop  23232  epttop  23234  neiptoptop  23356  tgcmp  23626  locfincmp  23752  dissnref  23754  comppfsc  23758  1stckgenlem  23779  txuni2  23791  txcmplem1  23867  tgqtop  23938  filuni  24111  alexsubALTlem4  24276  ptcmplem3  24280  ptcmplem4  24281  utoptop  24460  icccmplem1  25049  icccmplem3  25051  cnheibor  25183  bndth  25186  lebnumlem1  25189  bcthlem4  25555  ovolicc2lem5  25749  dyadmbllem  25827  itg2gt0  25988  rexunirn  32967  unipreima  33116  acunirnmpt2  33133  acunirnmpt2f  33134  elrspunidl  33856  ssmxidllem  33876  reff  34349  locfinreflem  34350  cmpcref  34360  ddemeas  34747  dya2iocuni  34794  bnj1379  35339  cvmsss2  35853  cvmseu  35855  untuni  36288  dfon2lem3  36362  dfon2lem7  36366  dfon2lem8  36367  brbigcup  36475  neibastop1  36978  neibastop2lem  36979  fvineqsneq  38166  heicant  38404  mblfinlem1  38406  cover2  38465  heiborlem9  38569  unichnidl  38781  erimeq2  39511  prtlem16  39742  prter2  39754  prter3  39755  ssunib  44061  onsupuni  44070  onsuplub  44089  restuni3  45950  disjinfi  46024  cncfuni  46714  intsaluni  47157  salgencntex  47171