Theorem eluni2 4870

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 1893	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4869	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 306	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-uni 4867

This theorem is used by:  uni0b  4893  intssuni  4929  iuncom4  4959  inuni  5310  cnvuni  5867  chfnrn  7049  ssorduni  7794  unon  7843  limuni3  7864  frrlem9  8316  onfununi  8353  oarec  8574  uniinqs  8822  fissuni  9350  finsschain  9352  r1sdom  9785  rankuni2b  9871  cflm  10331  coflim  10343  axdc3lem2  10533  fpwwe2lem11  10730  uniwun  10829  tskhf  10857  tskuni  10872  axgroth3  10920  inaprc  10925  tskmval  10928  tskmcl  10930  suplem1pr  11141  lbsextlem2  21443  lbsextlem3  21444  unichnlidl  21522  ssdifidllem  21646  isbasis3g  23273  eltg2b  23283  tgcl  23293  ppttop  23331  epttop  23333  neiptoptop  23455  tgcmp  23725  locfincmp  23851  dissnref  23853  comppfsc  23857  1stckgenlem  23878  txuni2  23890  txcmplem1  23966  tgqtop  24037  filuni  24210  alexsubALTlem4  24375  ptcmplem3  24379  ptcmplem4  24380  utoptop  24559  icccmplem1  25148  icccmplem3  25150  cnheibor  25282  bndth  25285  lebnumlem1  25288  bcthlem4  25654  ovolicc2lem5  25848  dyadmbllem  25926  itg2gt0  26087  rexunirn  33136  unipreima  33285  acunirnmpt2  33302  acunirnmpt2f  33303  elrspunidl  34025  ssmxidllem  34045  reff  34518  locfinreflem  34519  cmpcref  34529  ddemeas  34916  dya2iocuni  34962  bnj1379  35507  cvmsss2  36126  cvmseu  36128  untuni  36567  dfon2lem3  36640  dfon2lem7  36644  dfon2lem8  36645  brbigcup  36753  neibastop1  37240  neibastop2lem  37241  fvineqsneq  38429  heicant  38667  mblfinlem1  38669  cover2  38743  heiborlem9  38847  unichnidl  39059  erimeq2  39789  prtlem16  40020  prter2  40032  prter3  40033  ssunib  44316  onsupuni  44325  onsuplub  44344  restuni3  46227  disjinfi  46301  cncfuni  46990  intsaluni  47433  salgencntex  47447