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

Theorem eluni2 4874
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 1865 . 2 (∃𝑥(𝐴𝑥𝑥𝐵) ↔ ∃𝑥(𝑥𝐵𝐴𝑥))
2 eluni 4873 . 2 (𝐴 𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))
3 df-rex 3075 . 2 (∃𝑥𝐵 𝐴𝑥 ↔ ∃𝑥(𝑥𝐵𝐴𝑥))
41, 2, 33bitr4i 303 1 (𝐴 𝐵 ↔ ∃𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  wrex 3074   cuni 4870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-v 3450  df-uni 4871
This theorem is referenced by:  uni0b  4899  intssuni  4936  iuncom4  4967  inuni  5305  cnvuni  5847  chfnrn  7004  ssorduni  7718  unon  7771  limuni3  7793  frrlem9  8230  onfununi  8292  oarec  8514  uniinqs  8743  fissuni  9308  finsschain  9310  r1sdom  9717  rankuni2b  9796  cflm  10193  coflim  10204  axdc3lem2  10394  fpwwe2lem11  10584  uniwun  10683  tskr1om2  10711  tskuni  10726  axgroth3  10774  inaprc  10779  tskmval  10782  tskmcl  10784  suplem1pr  10995  lbsextlem2  20636  lbsextlem3  20637  isbasis3g  22315  eltg2b  22325  tgcl  22335  ppttop  22373  epttop  22375  neiptoptop  22498  tgcmp  22768  locfincmp  22893  dissnref  22895  comppfsc  22899  1stckgenlem  22920  txuni2  22932  txcmplem1  23008  tgqtop  23079  filuni  23252  alexsubALTlem4  23417  ptcmplem3  23421  ptcmplem4  23422  utoptop  23602  icccmplem1  24201  icccmplem3  24203  cnheibor  24334  bndth  24337  lebnumlem1  24340  bcthlem4  24707  ovolicc2lem5  24901  dyadmbllem  24979  itg2gt0  25141  rexunirn  31462  unipreima  31602  acunirnmpt2  31618  acunirnmpt2f  31619  elrspunidl  32243  ssmxidllem  32278  reff  32460  locfinreflem  32461  cmpcref  32471  ddemeas  32875  dya2iocuni  32923  bnj1379  33482  cvmsss2  33908  cvmseu  33910  untuni  34320  dfon2lem3  34399  dfon2lem7  34403  dfon2lem8  34404  brbigcup  34512  neibastop1  34860  neibastop2lem  34861  fvineqsneq  35912  heicant  36142  mblfinlem1  36144  cover2  36202  heiborlem9  36307  unichnidl  36519  erimeq2  37169  prtlem16  37360  prter2  37372  prter3  37373  ssunib  41583  onsupuni  41592  onsuplub  41611  restuni3  43402  disjinfi  43486  cncfuni  44201  intsaluni  44644  salgencntex  44658
  Copyright terms: Public domain W3C validator