Theorem eluni2 4871

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087  ∪ cuni 4867

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-v 3453  df-uni 4868

This theorem is used by:  uni0b  4894  intssuni  4930  iuncom4  4960  inuni  5311  cnvuni  5868  chfnrn  7046  ssorduni  7791  unon  7840  limuni3  7861  frrlem9  8305  onfununi  8342  oarec  8563  uniinqs  8811  fissuni  9339  finsschain  9341  r1sdom  9774  rankuni2b  9860  cflm  10320  coflim  10332  axdc3lem2  10522  fpwwe2lem11  10719  uniwun  10818  tskhf  10846  tskuni  10861  axgroth3  10909  inaprc  10914  tskmval  10917  tskmcl  10919  suplem1pr  11130  lbsextlem2  21430  lbsextlem3  21431  unichnlidl  21509  ssdifidllem  21633  isbasis3g  23260  eltg2b  23270  tgcl  23280  ppttop  23318  epttop  23320  neiptoptop  23442  tgcmp  23712  locfincmp  23838  dissnref  23840  comppfsc  23844  1stckgenlem  23865  txuni2  23877  txcmplem1  23953  tgqtop  24024  filuni  24197  alexsubALTlem4  24362  ptcmplem3  24366  ptcmplem4  24367  utoptop  24546  icccmplem1  25135  icccmplem3  25137  cnheibor  25269  bndth  25272  lebnumlem1  25275  bcthlem4  25641  ovolicc2lem5  25835  dyadmbllem  25913  itg2gt0  26074  rexunirn  33081  unipreima  33230  acunirnmpt2  33247  acunirnmpt2f  33248  elrspunidl  33971  ssmxidllem  33991  reff  34464  locfinreflem  34465  cmpcref  34475  ddemeas  34862  dya2iocuni  34908  bnj1379  35453  cvmsss2  36018  cvmseu  36020  untuni  36453  dfon2lem3  36527  dfon2lem7  36531  dfon2lem8  36532  brbigcup  36640  neibastop1  37127  neibastop2lem  37128  fvineqsneq  38315  heicant  38553  mblfinlem1  38555  cover2  38629  heiborlem9  38733  unichnidl  38945  erimeq2  39675  prtlem16  39906  prter2  39918  prter3  39919  ssunib  44206  onsupuni  44215  onsuplub  44234  restuni3  46102  disjinfi  46176  cncfuni  46865  intsaluni  47308  salgencntex  47322