Theorem eluni2 4876

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090  ∪ cuni 4872

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  df-uni 4873

This theorem is used by:  uni0b  4899  intssuni  4935  iuncom4  4965  inuni  5318  cnvuni  5880  chfnrn  7079  ssorduni  7827  unon  7876  limuni3  7897  frrlem9  8350  onfununi  8387  oarec  8608  uniinqs  8856  fissuni  9384  finsschain  9386  r1sdom  9818  rankuni2b  9904  cflm  10366  coflim  10378  axdc3lem2  10568  fpwwe2lem11  10765  uniwun  10864  tskhf  10892  tskuni  10907  axgroth3  10955  inaprc  10960  tskmval  10963  tskmcl  10965  suplem1pr  11176  lbsextlem2  21488  lbsextlem3  21489  unichnlidl  21567  ssdifidllem  21691  isbasis3g  23322  eltg2b  23332  tgcl  23342  ppttop  23380  epttop  23382  neiptoptop  23504  tgcmp  23774  locfincmp  23900  dissnref  23902  comppfsc  23906  1stckgenlem  23927  txuni2  23939  txcmplem1  24015  tgqtop  24086  filuni  24259  alexsubALTlem4  24424  ptcmplem3  24428  ptcmplem4  24429  utoptop  24608  icccmplem1  25197  icccmplem3  25199  cnheibor  25331  bndth  25334  lebnumlem1  25337  bcthlem4  25703  ovolicc2lem5  25897  dyadmbllem  25975  itg2gt0  26136  rexunirn  33187  unipreima  33335  acunirnmpt2  33352  acunirnmpt2f  33353  elrspunidl  34082  ssmxidllem  34102  reff  34582  locfinreflem  34583  cmpcref  34593  ddemeas  34980  dya2iocuni  35026  bnj1379  35571  cvmsss2  36247  cvmseu  36249  untuni  36689  dfon2lem3  36762  dfon2lem7  36766  dfon2lem8  36767  brbigcup  36875  neibastop1  37362  neibastop2lem  37363  fvineqsneq  38603  heicant  38841  mblfinlem1  38843  cover2  38917  heiborlem9  39019  unichnidl  39231  erimeq2  39961  prtlem16  40192  prter2  40204  prter3  40205  ssunib  44483  onsupuni  44492  onsuplub  44511  restuni3  46406  disjinfi  46480  cncfuni  47169  intsaluni  47612  salgencntex  47626