Theorem eluni2 4863

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-v 3438  df-uni 4860

This theorem is referenced by:  uni0b  4885  intssuni  4920  iuncom4  4950  inuni  5288  cnvuni  5826  chfnrn  6982  ssorduni  7712  unon  7761  limuni3  7782  frrlem9  8224  onfununi  8261  oarec  8477  uniinqs  8721  fissuni  9241  finsschain  9243  r1sdom  9667  rankuni2b  9746  cflm  10141  coflim  10152  axdc3lem2  10342  fpwwe2lem11  10532  uniwun  10631  tskr1om2  10659  tskuni  10674  axgroth3  10722  inaprc  10727  tskmval  10730  tskmcl  10732  suplem1pr  10943  lbsextlem2  21097  lbsextlem3  21098  isbasis3g  22865  eltg2b  22875  tgcl  22885  ppttop  22923  epttop  22925  neiptoptop  23047  tgcmp  23317  locfincmp  23442  dissnref  23444  comppfsc  23448  1stckgenlem  23469  txuni2  23481  txcmplem1  23557  tgqtop  23628  filuni  23801  alexsubALTlem4  23966  ptcmplem3  23970  ptcmplem4  23971  utoptop  24150  icccmplem1  24739  icccmplem3  24741  cnheibor  24882  bndth  24885  lebnumlem1  24888  bcthlem4  25255  ovolicc2lem5  25450  dyadmbllem  25528  itg2gt0  25689  rexunirn  32469  unipreima  32623  acunirnmpt2  32640  acunirnmpt2f  32641  elrspunidl  33391  ssdifidllem  33419  ssmxidllem  33436  reff  33850  locfinreflem  33851  cmpcref  33861  ddemeas  34247  dya2iocuni  34294  bnj1379  34840  cvmsss2  35316  cvmseu  35318  untuni  35751  dfon2lem3  35825  dfon2lem7  35829  dfon2lem8  35830  brbigcup  35938  neibastop1  36399  neibastop2lem  36400  fvineqsneq  37452  heicant  37701  mblfinlem1  37703  cover2  37761  heiborlem9  37865  unichnidl  38077  erimeq2  38722  prtlem16  38914  prter2  38926  prter3  38927  ssunib  43259  onsupuni  43268  onsuplub  43287  restuni3  45161  disjinfi  45235  cncfuni  45930  intsaluni  46373  salgencntex  46387