Theorem eluni2 4864

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057  ∪ cuni 4860

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-v 3439  df-uni 4861

This theorem is referenced by:  uni0b  4886  intssuni  4922  iuncom4  4952  inuni  5292  cnvuni  5832  chfnrn  6990  ssorduni  7720  unon  7769  limuni3  7790  frrlem9  8232  onfununi  8269  oarec  8485  uniinqs  8729  fissuni  9250  finsschain  9252  r1sdom  9676  rankuni2b  9755  cflm  10150  coflim  10161  axdc3lem2  10351  fpwwe2lem11  10541  uniwun  10640  tskr1om2  10668  tskuni  10683  axgroth3  10731  inaprc  10736  tskmval  10739  tskmcl  10741  suplem1pr  10952  lbsextlem2  21100  lbsextlem3  21101  isbasis3g  22867  eltg2b  22877  tgcl  22887  ppttop  22925  epttop  22927  neiptoptop  23049  tgcmp  23319  locfincmp  23444  dissnref  23446  comppfsc  23450  1stckgenlem  23471  txuni2  23483  txcmplem1  23559  tgqtop  23630  filuni  23803  alexsubALTlem4  23968  ptcmplem3  23972  ptcmplem4  23973  utoptop  24152  icccmplem1  24741  icccmplem3  24743  cnheibor  24884  bndth  24887  lebnumlem1  24890  bcthlem4  25257  ovolicc2lem5  25452  dyadmbllem  25530  itg2gt0  25691  rexunirn  32475  unipreima  32629  acunirnmpt2  32646  acunirnmpt2f  32647  elrspunidl  33402  ssdifidllem  33430  ssmxidllem  33447  reff  33875  locfinreflem  33876  cmpcref  33886  ddemeas  34272  dya2iocuni  34319  bnj1379  34865  cvmsss2  35341  cvmseu  35343  untuni  35776  dfon2lem3  35850  dfon2lem7  35854  dfon2lem8  35855  brbigcup  35963  neibastop1  36426  neibastop2lem  36427  fvineqsneq  37479  heicant  37718  mblfinlem1  37720  cover2  37778  heiborlem9  37882  unichnidl  38094  erimeq2  38799  prtlem16  38991  prter2  39003  prter3  39004  ssunib  43340  onsupuni  43349  onsuplub  43368  restuni3  45242  disjinfi  45316  cncfuni  46011  intsaluni  46454  salgencntex  46468