Theorem eluni2 4869

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3444  df-uni 4866

This theorem is referenced by:  uni0b  4891  intssuni  4927  iuncom4  4957  inuni  5297  cnvuni  5843  chfnrn  7003  ssorduni  7734  unon  7783  limuni3  7804  frrlem9  8246  onfununi  8283  oarec  8499  uniinqs  8746  fissuni  9269  finsschain  9271  r1sdom  9698  rankuni2b  9777  cflm  10172  coflim  10183  axdc3lem2  10373  fpwwe2lem11  10564  uniwun  10663  tskr1om2  10691  tskuni  10706  axgroth3  10754  inaprc  10759  tskmval  10762  tskmcl  10764  suplem1pr  10975  lbsextlem2  21126  lbsextlem3  21127  isbasis3g  22905  eltg2b  22915  tgcl  22925  ppttop  22963  epttop  22965  neiptoptop  23087  tgcmp  23357  locfincmp  23482  dissnref  23484  comppfsc  23488  1stckgenlem  23509  txuni2  23521  txcmplem1  23597  tgqtop  23668  filuni  23841  alexsubALTlem4  24006  ptcmplem3  24010  ptcmplem4  24011  utoptop  24190  icccmplem1  24779  icccmplem3  24781  cnheibor  24922  bndth  24925  lebnumlem1  24928  bcthlem4  25295  ovolicc2lem5  25490  dyadmbllem  25568  itg2gt0  25729  rexunirn  32577  unipreima  32732  acunirnmpt2  32749  acunirnmpt2f  32750  elrspunidl  33520  ssdifidllem  33548  ssmxidllem  33565  reff  34016  locfinreflem  34017  cmpcref  34027  ddemeas  34413  dya2iocuni  34460  bnj1379  35005  cvmsss2  35487  cvmseu  35489  untuni  35922  dfon2lem3  35996  dfon2lem7  36000  dfon2lem8  36001  brbigcup  36109  neibastop1  36572  neibastop2lem  36573  fvineqsneq  37664  heicant  37903  mblfinlem1  37905  cover2  37963  heiborlem9  38067  unichnidl  38279  erimeq2  39011  prtlem16  39242  prter2  39254  prter3  39255  ssunib  43574  onsupuni  43583  onsuplub  43602  restuni3  45474  disjinfi  45548  cncfuni  46241  intsaluni  46684  salgencntex  46698