Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluni2 Structured version   Visualization version   GIF version

Theorem eluni2 4807
 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
StepHypRef Expression
1 exancom 1862 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) ↔ ∃𝑥(𝑥𝐵𝐴𝑥))
2 eluni 4806 . 2 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
3 df-rex 3115 . 2 (∃𝑥𝐵 𝐴𝑥 ↔ ∃𝑥(𝑥𝐵𝐴𝑥))
41, 2, 33bitr4i 306 1 (𝐴 𝐵 ↔ ∃𝑥𝐵 𝐴𝑥)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2112  ∃wrex 3110  ∪ cuni 4803 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rex 3115  df-v 3446  df-uni 4804 This theorem is referenced by:  uni0b  4829  intssuni  4863  iuncom4  4892  inuni  5213  cnvuni  5725  chfnrn  6800  ssorduni  7484  unon  7530  limuni3  7551  onfununi  7965  oarec  8175  uniinqs  8364  fissuni  8817  finsschain  8819  r1sdom  9191  rankuni2b  9270  cflm  9665  coflim  9676  axdc3lem2  9866  fpwwe2lem12  10056  uniwun  10155  tskr1om2  10183  tskuni  10198  axgroth3  10246  inaprc  10251  tskmval  10254  tskmcl  10256  suplem1pr  10467  lbsextlem2  19928  lbsextlem3  19929  isbasis3g  21558  eltg2b  21568  tgcl  21578  ppttop  21616  epttop  21618  neiptoptop  21740  tgcmp  22010  locfincmp  22135  dissnref  22137  comppfsc  22141  1stckgenlem  22162  txuni2  22174  txcmplem1  22250  tgqtop  22321  filuni  22494  alexsubALTlem4  22659  ptcmplem3  22663  ptcmplem4  22664  utoptop  22844  icccmplem1  23431  icccmplem3  23433  cnheibor  23564  bndth  23567  lebnumlem1  23570  bcthlem4  23935  ovolicc2lem5  24129  dyadmbllem  24207  itg2gt0  24368  rexunirn  30267  unipreima  30409  acunirnmpt2  30427  acunirnmpt2f  30428  elrspunidl  31018  ssmxidllem  31053  reff  31196  locfinreflem  31197  cmpcref  31207  ddemeas  31609  dya2iocuni  31655  bnj1379  32216  cvmsss2  32635  cvmseu  32637  untuni  33049  dfon2lem3  33144  dfon2lem7  33148  dfon2lem8  33149  frrlem9  33245  brbigcup  33473  neibastop1  33821  neibastop2lem  33822  fvineqsneq  34830  heicant  35091  mblfinlem1  35093  cover2  35151  heiborlem9  35256  unichnidl  35468  erim2  36070  prtlem16  36164  prter2  36176  prter3  36177  restuni3  41746  disjinfi  41813  cncfuni  42521  intsaluni  42962  salgencntex  42976
 Copyright terms: Public domain W3C validator