MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbidv Structured version   Unicode version

Theorem exbidv 1690
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
exbidv  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-5 1680 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1653 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  2exbidv  1692  3exbidv  1693  eubid  2296  eleq1d  2536  eleq2dALT  2538  eleq1OLD  2541  eleq2OLD  2542  rexbidv2  2969  ceqsex2  3151  alexeqg  3232  alexeq  3233  sbc2or  3340  sbc5  3356  sbcex2  3385  sbcexgOLD  3386  sbcabel  3420  eluni  4248  csbuni  4273  csbunigOLD  4274  intab  4312  cbvopab1  4517  cbvopab1s  4519  axrep1  4559  axrep2  4560  axrep3  4561  zfrepclf  4564  axsep2  4569  zfauscl  4570  euotd  4748  opeliunxp  5051  csbxpgOLD  5082  brcog  5169  elrn2g  5193  dfdmf  5196  eldmg  5198  dfrnf  5241  elrn2  5242  elrnmpt1  5251  brcodir  5386  csbrngOLD  5469  dfco2a  5507  cores  5510  sbcfung  5611  brprcneu  5859  ssimaexg  5933  dmfco  5941  fndmdif  5985  fmptco  6054  fliftf  6201  cbvoprab1  6353  cbvoprab2  6354  snnex  6590  uniuni  6593  dmtpos  6967  rdglim2  7098  ecdmn0  7354  mapsn  7460  bren  7525  brdomg  7526  domeng  7530  isinf  7733  ac6sfi  7764  ordiso  7941  brwdom  7993  brwdom2  7999  zfregcl  8020  inf0  8038  zfinf  8056  bnd2  8311  isinffi  8373  acneq  8424  acni  8426  aceq0  8499  aceq3lem  8501  dfac3  8502  dfac5lem4  8507  dfac8  8515  dfac9  8516  kmlem1  8530  kmlem2  8531  kmlem8  8537  kmlem10  8539  kmlem13  8542  cfval  8627  cardcf  8632  cfeq0  8636  cfsuc  8637  cff1  8638  cflim3  8642  cofsmo  8649  isfin4  8677  axcc2lem  8816  axcc4dom  8821  domtriomlem  8822  dcomex  8827  axdc2lem  8828  axdc4lem  8835  zfac  8840  ac7g  8854  ac4c  8856  ac5  8857  ac6sg  8868  weth  8875  axrepndlem1  8967  axunndlem1  8970  zfcndrep  8992  zfcndinf  8996  zfcndac  8997  gruina  9196  grothomex  9207  genpass  9387  1idpr  9407  ltexprlem3  9416  ltexprlem4  9417  ltexpri  9421  reclem2pr  9426  reclem3pr  9427  recexpr  9429  infm3  10502  nnunb  10791  axdc4uz  12061  sumeq1  13474  sumeq2w  13477  sumeq2ii  13478  summo  13502  fsum  13505  fsum2dlem  13548  vdwapun  14351  vdwmc  14355  vdwmc2  14356  isacs  14906  brssc  15044  isssc  15050  dirge  15724  gsumvalx  15824  gsumpropd  15826  gsumpropd2lem  15827  gsumress  15829  gsumval3eu  16710  gsumval3OLD  16711  gsumval3lem2  16713  dprd2d2  16895  znleval  18388  neitr  19475  cmpcovf  19685  hausmapdom  19795  ptval  19834  elpt  19836  ptpjopn  19876  ptclsg  19879  ptcnp  19886  uffix2  20188  cnextf  20329  prdsxmslem2  20795  metustfbasOLD  20831  metustfbas  20832  metcld2  21508  dchrmusumlema  23434  dchrisum0lema  23455  istrkgld  23613  uvtx01vtx  24196  wlkiswwlk2  24401  wlklniswwlkn2  24404  wlknwwlknvbij  24444  clwlkisclwwlk  24493  clwwlkvbij  24505  isgrpo  24902  ismgm  25026  adjeu  26512  fcoinvbr  27162  fmptcof2  27202  ishashinf  27302  fmcncfil  27577  relexpindlem  28565  ntrivcvgn0  28637  ntrivcvgmullem  28640  prodeq1f  28645  prodeq2w  28649  prodeq2ii  28650  prodmo  28673  zprod  28674  fprod  28678  fprodntriv  28679  fprod2dlem  28715  eldm3  28796  opelco3  28813  wrecseq123  28942  wfrlem1  28948  wfrlem15  28962  frrlem1  28992  elsingles  29173  funpartlem  29197  dfrdg4  29205  linedegen  29398  wl-sb8eut  29627  finminlem  29741  filnetlem4  29830  sdclem1  29867  fdc  29869  isriscg  30018  dfac11  30640  iotasbc  30932  iotasbc2  30933  fnchoice  31010  stoweidlem35  31363  stoweidlem39  31367  opeliun2xp  32018  bnj865  33078  bnj1388  33186  bnj1489  33209  bj-axrep1  33473  bj-axrep2  33474  bj-axrep3  33475  bj-eleq1w  33521  bj-eleq2w  33522  bj-issetwt  33534  bj-axsep2  33592  bj-finsumval0  33753  islshpat  33832  lshpsmreu  33924  isopos  33995  islpln5  34349  islvol5  34393  pmapjat1  34667  dibelval3  35962  diblsmopel  35986  mapdpglem3  36490  hdmapglem7a  36745
  Copyright terms: Public domain W3C validator