Theorem eluni2 4911

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 1864	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4910	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 302	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070  ∪ cuni 4907

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-v 3476  df-uni 4908

This theorem is referenced by:  uni0b  4936  intssuni  4973  iuncom4  5004  inuni  5342  cnvuni  5884  chfnrn  7047  ssorduni  7762  unon  7815  limuni3  7837  frrlem9  8275  onfununi  8337  oarec  8558  uniinqs  8787  fissuni  9353  finsschain  9355  r1sdom  9765  rankuni2b  9844  cflm  10241  coflim  10252  axdc3lem2  10442  fpwwe2lem11  10632  uniwun  10731  tskr1om2  10759  tskuni  10774  axgroth3  10822  inaprc  10827  tskmval  10830  tskmcl  10832  suplem1pr  11043  lbsextlem2  20764  lbsextlem3  20765  isbasis3g  22443  eltg2b  22453  tgcl  22463  ppttop  22501  epttop  22503  neiptoptop  22626  tgcmp  22896  locfincmp  23021  dissnref  23023  comppfsc  23027  1stckgenlem  23048  txuni2  23060  txcmplem1  23136  tgqtop  23207  filuni  23380  alexsubALTlem4  23545  ptcmplem3  23549  ptcmplem4  23550  utoptop  23730  icccmplem1  24329  icccmplem3  24331  cnheibor  24462  bndth  24465  lebnumlem1  24468  bcthlem4  24835  ovolicc2lem5  25029  dyadmbllem  25107  itg2gt0  25269  rexunirn  31719  unipreima  31856  acunirnmpt2  31872  acunirnmpt2f  31873  elrspunidl  32534  ssmxidllem  32577  reff  32807  locfinreflem  32808  cmpcref  32818  ddemeas  33222  dya2iocuni  33270  bnj1379  33829  cvmsss2  34253  cvmseu  34255  untuni  34666  dfon2lem3  34745  dfon2lem7  34749  dfon2lem8  34750  brbigcup  34858  neibastop1  35232  neibastop2lem  35233  fvineqsneq  36281  heicant  36511  mblfinlem1  36513  cover2  36571  heiborlem9  36675  unichnidl  36887  erimeq2  37536  prtlem16  37727  prter2  37739  prter3  37740  ssunib  41954  onsupuni  41963  onsuplub  41982  restuni3  43792  disjinfi  43876  cncfuni  44588  intsaluni  45031  salgencntex  45045