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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3090  df-v 3459  df-uni 4868

This theorem is referenced by:  uni0b  4894  intssuni  4930  iuncom4  4960  inuni  5310  cnvuni  5866  chfnrn  7034  ssorduni  7766  unon  7815  limuni3  7836  frrlem9  8279  onfununi  8316  oarec  8535  uniinqs  8783  fissuni  9302  finsschain  9304  r1sdom  9734  rankuni2b  9813  cflm  10221  coflim  10233  axdc3lem2  10423  fpwwe2lem11  10614  uniwun  10713  tskr1om2  10741  tskuni  10756  axgroth3  10804  inaprc  10809  tskmval  10812  tskmcl  10814  suplem1pr  11025  lbsextlem2  21249  lbsextlem3  21250  unichnlidl  21328  ssdifidllem  21441  isbasis3g  23063  eltg2b  23073  tgcl  23083  ppttop  23121  epttop  23123  neiptoptop  23245  tgcmp  23515  locfincmp  23640  dissnref  23642  comppfsc  23646  1stckgenlem  23667  txuni2  23679  txcmplem1  23755  tgqtop  23826  filuni  23999  alexsubALTlem4  24164  ptcmplem3  24168  ptcmplem4  24169  utoptop  24348  icccmplem1  24937  icccmplem3  24939  cnheibor  25071  bndth  25074  lebnumlem1  25077  bcthlem4  25443  ovolicc2lem5  25637  dyadmbllem  25715  itg2gt0  25876  rexunirn  32744  unipreima  32896  acunirnmpt2  32913  acunirnmpt2f  32914  elrspunidl  33647  ssmxidllem  33668  reff  34141  locfinreflem  34142  cmpcref  34152  ddemeas  34538  dya2iocuni  34585  bnj1379  35130  cvmsss2  35632  cvmseu  35634  untuni  36067  dfon2lem3  36141  dfon2lem7  36145  dfon2lem8  36146  brbigcup  36254  neibastop1  36727  neibastop2lem  36728  fvineqsneq  37913  heicant  38161  mblfinlem1  38163  cover2  38221  heiborlem9  38325  unichnidl  38537  erimeq2  39269  prtlem16  39500  prter2  39512  prter3  39513  ssunib  43804  onsupuni  43813  onsuplub  43832  restuni3  45695  disjinfi  45769  cncfuni  46459  intsaluni  46902  salgencntex  46916