Theorem eluni2 4844

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2107  ∃wrex 3066  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rex 3071  df-v 3435  df-uni 4841

This theorem is referenced by:  uni0b  4868  intssuni  4902  iuncom4  4933  inuni  5268  cnvuni  5798  chfnrn  6935  ssorduni  7638  unon  7687  limuni3  7708  frrlem9  8119  onfununi  8181  oarec  8402  uniinqs  8595  fissuni  9133  finsschain  9135  r1sdom  9541  rankuni2b  9620  cflm  10015  coflim  10026  axdc3lem2  10216  fpwwe2lem11  10406  uniwun  10505  tskr1om2  10533  tskuni  10548  axgroth3  10596  inaprc  10601  tskmval  10604  tskmcl  10606  suplem1pr  10817  lbsextlem2  20430  lbsextlem3  20431  isbasis3g  22108  eltg2b  22118  tgcl  22128  ppttop  22166  epttop  22168  neiptoptop  22291  tgcmp  22561  locfincmp  22686  dissnref  22688  comppfsc  22692  1stckgenlem  22713  txuni2  22725  txcmplem1  22801  tgqtop  22872  filuni  23045  alexsubALTlem4  23210  ptcmplem3  23214  ptcmplem4  23215  utoptop  23395  icccmplem1  23994  icccmplem3  23996  cnheibor  24127  bndth  24130  lebnumlem1  24133  bcthlem4  24500  ovolicc2lem5  24694  dyadmbllem  24772  itg2gt0  24934  rexunirn  30849  unipreima  30990  acunirnmpt2  31006  acunirnmpt2f  31007  elrspunidl  31615  ssmxidllem  31650  reff  31798  locfinreflem  31799  cmpcref  31809  ddemeas  32213  dya2iocuni  32259  bnj1379  32819  cvmsss2  33245  cvmseu  33247  untuni  33659  dfon2lem3  33770  dfon2lem7  33774  dfon2lem8  33775  brbigcup  34209  neibastop1  34557  neibastop2lem  34558  fvineqsneq  35592  heicant  35821  mblfinlem1  35823  cover2  35881  heiborlem9  35986  unichnidl  36198  erim2  36796  prtlem16  36890  prter2  36902  prter3  36903  restuni3  42674  disjinfi  42738  cncfuni  43434  intsaluni  43875  salgencntex  43889