Theorem eluni2 4866

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 1880	. 2 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
2		eluni 4865	. 2 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
3		df-rex 3086	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥))
4	1, 2, 3	3bitr4i 305	1 ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-v 3455  df-uni 4863

This theorem is referenced by:  uni0b  4889  intssuni  4925  iuncom4  4955  inuni  5303  cnvuni  5858  chfnrn  7024  ssorduni  7756  unon  7805  limuni3  7826  frrlem9  8268  onfununi  8305  oarec  8524  uniinqs  8772  fissuni  9293  finsschain  9295  r1sdom  9725  rankuni2b  9804  cflm  10199  coflim  10211  axdc3lem2  10401  fpwwe2lem11  10592  uniwun  10691  tskr1om2  10719  tskuni  10734  axgroth3  10782  inaprc  10787  tskmval  10790  tskmcl  10792  suplem1pr  11003  lbsextlem2  21216  lbsextlem3  21217  isbasis3g  22996  eltg2b  23006  tgcl  23016  ppttop  23054  epttop  23056  neiptoptop  23178  tgcmp  23448  locfincmp  23573  dissnref  23575  comppfsc  23579  1stckgenlem  23600  txuni2  23612  txcmplem1  23688  tgqtop  23759  filuni  23932  alexsubALTlem4  24097  ptcmplem3  24101  ptcmplem4  24102  utoptop  24281  icccmplem1  24870  icccmplem3  24872  cnheibor  25004  bndth  25007  lebnumlem1  25010  bcthlem4  25376  ovolicc2lem5  25570  dyadmbllem  25648  itg2gt0  25809  rexunirn  32649  unipreima  32805  acunirnmpt2  32822  acunirnmpt2f  32823  elrspunidl  33574  ssdifidllem  33603  ssmxidllem  33621  reff  34096  locfinreflem  34097  cmpcref  34107  ddemeas  34493  dya2iocuni  34540  bnj1379  35085  cvmsss2  35584  cvmseu  35586  untuni  36019  dfon2lem3  36093  dfon2lem7  36097  dfon2lem8  36098  brbigcup  36206  neibastop1  36679  neibastop2lem  36680  fvineqsneq  37866  heicant  38114  mblfinlem1  38116  cover2  38174  heiborlem9  38278  unichnidl  38490  erimeq2  39222  prtlem16  39453  prter2  39465  prter3  39466  ssunib  43757  onsupuni  43766  onsuplub  43785  restuni3  45656  disjinfi  45730  cncfuni  46420  intsaluni  46863  salgencntex  46877