Theorem eluni2 4840

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rex 3069  df-v 3424  df-uni 4837

This theorem is referenced by:  uni0b  4864  intssuni  4898  iuncom4  4929  inuni  5262  cnvuni  5784  chfnrn  6908  ssorduni  7606  unon  7653  limuni3  7674  frrlem9  8081  onfununi  8143  oarec  8355  uniinqs  8544  fissuni  9054  finsschain  9056  r1sdom  9463  rankuni2b  9542  cflm  9937  coflim  9948  axdc3lem2  10138  fpwwe2lem11  10328  uniwun  10427  tskr1om2  10455  tskuni  10470  axgroth3  10518  inaprc  10523  tskmval  10526  tskmcl  10528  suplem1pr  10739  lbsextlem2  20336  lbsextlem3  20337  isbasis3g  22007  eltg2b  22017  tgcl  22027  ppttop  22065  epttop  22067  neiptoptop  22190  tgcmp  22460  locfincmp  22585  dissnref  22587  comppfsc  22591  1stckgenlem  22612  txuni2  22624  txcmplem1  22700  tgqtop  22771  filuni  22944  alexsubALTlem4  23109  ptcmplem3  23113  ptcmplem4  23114  utoptop  23294  icccmplem1  23891  icccmplem3  23893  cnheibor  24024  bndth  24027  lebnumlem1  24030  bcthlem4  24396  ovolicc2lem5  24590  dyadmbllem  24668  itg2gt0  24830  rexunirn  30741  unipreima  30882  acunirnmpt2  30899  acunirnmpt2f  30900  elrspunidl  31508  ssmxidllem  31543  reff  31691  locfinreflem  31692  cmpcref  31702  ddemeas  32104  dya2iocuni  32150  bnj1379  32710  cvmsss2  33136  cvmseu  33138  untuni  33550  dfon2lem3  33667  dfon2lem7  33671  dfon2lem8  33672  brbigcup  34127  neibastop1  34475  neibastop2lem  34476  fvineqsneq  35510  heicant  35739  mblfinlem1  35741  cover2  35799  heiborlem9  35904  unichnidl  36116  erim2  36716  prtlem16  36810  prter2  36822  prter3  36823  restuni3  42556  disjinfi  42620  cncfuni  43317  intsaluni  43758  salgencntex  43772