Theorem eluni2 4855

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-uni 4852

This theorem is referenced by:  uni0b  4877  intssuni  4913  iuncom4  4943  inuni  5287  cnvuni  5835  chfnrn  6995  ssorduni  7726  unon  7775  limuni3  7796  frrlem9  8237  onfununi  8274  oarec  8490  uniinqs  8737  fissuni  9260  finsschain  9262  r1sdom  9689  rankuni2b  9768  cflm  10163  coflim  10174  axdc3lem2  10364  fpwwe2lem11  10555  uniwun  10654  tskr1om2  10682  tskuni  10697  axgroth3  10745  inaprc  10750  tskmval  10753  tskmcl  10755  suplem1pr  10966  lbsextlem2  21149  lbsextlem3  21150  isbasis3g  22924  eltg2b  22934  tgcl  22944  ppttop  22982  epttop  22984  neiptoptop  23106  tgcmp  23376  locfincmp  23501  dissnref  23503  comppfsc  23507  1stckgenlem  23528  txuni2  23540  txcmplem1  23616  tgqtop  23687  filuni  23860  alexsubALTlem4  24025  ptcmplem3  24029  ptcmplem4  24030  utoptop  24209  icccmplem1  24798  icccmplem3  24800  cnheibor  24932  bndth  24935  lebnumlem1  24938  bcthlem4  25304  ovolicc2lem5  25498  dyadmbllem  25576  itg2gt0  25737  rexunirn  32576  unipreima  32731  acunirnmpt2  32748  acunirnmpt2f  32749  elrspunidl  33503  ssdifidllem  33531  ssmxidllem  33548  reff  33999  locfinreflem  34000  cmpcref  34010  ddemeas  34396  dya2iocuni  34443  bnj1379  34988  cvmsss2  35472  cvmseu  35474  untuni  35907  dfon2lem3  35981  dfon2lem7  35985  dfon2lem8  35986  brbigcup  36094  neibastop1  36557  neibastop2lem  36558  fvineqsneq  37742  heicant  37990  mblfinlem1  37992  cover2  38050  heiborlem9  38154  unichnidl  38366  erimeq2  39098  prtlem16  39329  prter2  39341  prter3  39342  ssunib  43666  onsupuni  43675  onsuplub  43694  restuni3  45566  disjinfi  45640  cncfuni  46332  intsaluni  46775  salgencntex  46789