Theorem eluni2 4917

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1774   ∈ wcel 2099  ∃wrex 3060  ∪ cuni 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rex 3061  df-v 3464  df-uni 4914

This theorem is referenced by:  uni0b  4941  intssuni  4978  iuncom4  5009  inuni  5350  cnvuni  5893  chfnrn  7062  ssorduni  7787  unon  7840  limuni3  7862  frrlem9  8309  onfununi  8371  oarec  8592  uniinqs  8826  fissuni  9401  finsschain  9403  r1sdom  9817  rankuni2b  9896  cflm  10293  coflim  10304  axdc3lem2  10494  fpwwe2lem11  10684  uniwun  10783  tskr1om2  10811  tskuni  10826  axgroth3  10874  inaprc  10879  tskmval  10882  tskmcl  10884  suplem1pr  11095  lbsextlem2  21140  lbsextlem3  21141  isbasis3g  22943  eltg2b  22953  tgcl  22963  ppttop  23001  epttop  23003  neiptoptop  23126  tgcmp  23396  locfincmp  23521  dissnref  23523  comppfsc  23527  1stckgenlem  23548  txuni2  23560  txcmplem1  23636  tgqtop  23707  filuni  23880  alexsubALTlem4  24045  ptcmplem3  24049  ptcmplem4  24050  utoptop  24230  icccmplem1  24829  icccmplem3  24831  cnheibor  24972  bndth  24975  lebnumlem1  24978  bcthlem4  25346  ovolicc2lem5  25541  dyadmbllem  25619  itg2gt0  25781  rexunirn  32420  unipreima  32561  acunirnmpt2  32577  acunirnmpt2f  32578  elrspunidl  33303  ssdifidllem  33331  ssmxidllem  33348  reff  33654  locfinreflem  33655  cmpcref  33665  ddemeas  34069  dya2iocuni  34117  bnj1379  34675  cvmsss2  35102  cvmseu  35104  untuni  35531  dfon2lem3  35609  dfon2lem7  35613  dfon2lem8  35614  brbigcup  35722  neibastop1  36071  neibastop2lem  36072  fvineqsneq  37119  heicant  37356  mblfinlem1  37358  cover2  37416  heiborlem9  37520  unichnidl  37732  erimeq2  38376  prtlem16  38567  prter2  38579  prter3  38580  ssunib  42885  onsupuni  42894  onsuplub  42913  restuni3  44719  disjinfi  44799  cncfuni  45507  intsaluni  45950  salgencntex  45964