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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-uni 4875

This theorem is referenced by:  uni0b  4900  intssuni  4937  iuncom4  4967  inuni  5308  cnvuni  5853  chfnrn  7024  ssorduni  7758  unon  7809  limuni3  7831  frrlem9  8276  onfununi  8313  oarec  8529  uniinqs  8773  fissuni  9315  finsschain  9317  r1sdom  9734  rankuni2b  9813  cflm  10210  coflim  10221  axdc3lem2  10411  fpwwe2lem11  10601  uniwun  10700  tskr1om2  10728  tskuni  10743  axgroth3  10791  inaprc  10796  tskmval  10799  tskmcl  10801  suplem1pr  11012  lbsextlem2  21076  lbsextlem3  21077  isbasis3g  22843  eltg2b  22853  tgcl  22863  ppttop  22901  epttop  22903  neiptoptop  23025  tgcmp  23295  locfincmp  23420  dissnref  23422  comppfsc  23426  1stckgenlem  23447  txuni2  23459  txcmplem1  23535  tgqtop  23606  filuni  23779  alexsubALTlem4  23944  ptcmplem3  23948  ptcmplem4  23949  utoptop  24129  icccmplem1  24718  icccmplem3  24720  cnheibor  24861  bndth  24864  lebnumlem1  24867  bcthlem4  25234  ovolicc2lem5  25429  dyadmbllem  25507  itg2gt0  25668  rexunirn  32428  unipreima  32574  acunirnmpt2  32591  acunirnmpt2f  32592  elrspunidl  33406  ssdifidllem  33434  ssmxidllem  33451  reff  33836  locfinreflem  33837  cmpcref  33847  ddemeas  34233  dya2iocuni  34281  bnj1379  34827  cvmsss2  35268  cvmseu  35270  untuni  35703  dfon2lem3  35780  dfon2lem7  35784  dfon2lem8  35785  brbigcup  35893  neibastop1  36354  neibastop2lem  36355  fvineqsneq  37407  heicant  37656  mblfinlem1  37658  cover2  37716  heiborlem9  37820  unichnidl  38032  erimeq2  38677  prtlem16  38869  prter2  38881  prter3  38882  ssunib  43216  onsupuni  43225  onsuplub  43244  restuni3  45119  disjinfi  45193  cncfuni  45891  intsaluni  46334  salgencntex  46348