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

Theorem exbidv 1680
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 1670 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1643 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  2exbidv  1682  3exbidv  1683  eubid  2274  eleq1  2503  eleq2  2504  rexbidv2  2759  ceqsex2  3031  alexeqg  3109  alexeq  3110  sbc2or  3216  sbc5  3232  sbcex2  3261  sbcexgOLD  3262  sbcabel  3296  eluni  4115  csbuni  4140  csbunigOLD  4141  intab  4179  cbvopab1  4383  cbvopab1s  4385  axrep1  4425  axrep2  4426  axrep3  4427  zfrepclf  4430  axsep2  4435  zfauscl  4436  euotd  4613  opeliunxp  4911  csbxpgOLD  4940  brcog  5027  elrn2g  5051  dfdmf  5054  eldmg  5056  dfrnf  5099  elrn2  5100  elrnmpt1  5109  brcodir  5238  csbrngOLD  5321  dfco2a  5359  cores  5362  sbcfung  5462  brprcneu  5705  ssimaexg  5778  dmfco  5786  fndmdif  5828  fmptco  5897  fliftf  6029  cbvoprab1  6179  cbvoprab2  6180  snnex  6403  uniuni  6406  dmtpos  6778  rdglim2  6909  ecdmn0  7164  mapsn  7275  bren  7340  brdomg  7341  domeng  7345  isinf  7547  ac6sfi  7577  ordiso  7751  brwdom  7803  brwdom2  7809  zfregcl  7830  inf0  7848  zfinf  7866  bnd2  8121  isinffi  8183  acneq  8234  acni  8236  aceq0  8309  aceq3lem  8311  dfac3  8312  dfac5lem4  8317  dfac8  8325  dfac9  8326  kmlem1  8340  kmlem2  8341  kmlem8  8347  kmlem10  8349  kmlem13  8352  cfval  8437  cardcf  8442  cfeq0  8446  cfsuc  8447  cff1  8448  cflim3  8452  cofsmo  8459  isfin4  8487  axcc2lem  8626  axcc4dom  8631  domtriomlem  8632  dcomex  8637  axdc2lem  8638  axdc4lem  8645  zfac  8650  ac7g  8664  ac4c  8666  ac5  8667  ac6sg  8678  weth  8685  axrepndlem1  8777  axunndlem1  8780  zfcndrep  8802  zfcndinf  8806  zfcndac  8807  gruina  9006  grothomex  9017  genpass  9199  1idpr  9219  ltexprlem3  9228  ltexprlem4  9229  ltexpri  9233  reclem2pr  9238  reclem3pr  9239  recexpr  9241  infm3  10310  nnunb  10596  axdc4uz  11826  sumeq1  13187  sumeq2w  13190  sumeq2ii  13191  summo  13215  fsum  13218  fsum2dlem  13258  vdwapun  14056  vdwmc  14060  vdwmc2  14061  isacs  14610  brssc  14748  isssc  14754  dirge  15428  gsumvalx  15523  gsumpropd  15525  gsumpropd2lem  15526  gsumress  15528  gsumval3eu  16402  gsumval3OLD  16403  gsumval3lem2  16405  dprd2d2  16565  znleval  18009  neitr  18806  cmpcovf  19016  hausmapdom  19126  ptval  19165  elpt  19167  ptpjopn  19207  ptclsg  19210  ptcnp  19217  uffix2  19519  cnextf  19660  prdsxmslem2  20126  metustfbasOLD  20162  metustfbas  20163  metcld2  20839  dchrmusumlema  22764  dchrisum0lema  22785  uvtx01vtx  23422  isgrpo  23705  ismgm  23829  adjeu  25315  fmptcof2  26001  ishashinf  26107  fmcncfil  26383  relexpindlem  27363  ntrivcvgn0  27435  ntrivcvgmullem  27438  prodeq1f  27443  prodeq2w  27447  prodeq2ii  27448  prodmo  27471  zprod  27472  fprod  27476  fprodntriv  27477  fprod2dlem  27513  eldm3  27594  opelco3  27611  wrecseq123  27740  wfrlem1  27746  wfrlem15  27760  frrlem1  27790  elsingles  27971  funpartlem  27995  dfrdg4  28003  linedegen  28196  wl-sb8eut  28424  finminlem  28539  filnetlem4  28628  sdclem1  28665  fdc  28667  isriscg  28816  dfac11  29441  iotasbc  29699  iotasbc2  29700  fnchoice  29777  stoweidlem35  29856  stoweidlem39  29860  wlkiswwlk2  30357  wlklniswwlkn2  30360  wlknwwlknvbij  30398  clwlkisclwwlk  30477  clwwlkvbij  30489  opeliun2xp  30746  bnj865  32012  bnj1388  32120  bnj1489  32143  bj-axrep1  32405  bj-axrep2  32406  bj-axrep3  32407  bj-eleq1w  32453  bj-eleq2w  32454  bj-issetwt  32466  bj-axsep2  32524  bj-finsumval0  32679  islshpat  32758  lshpsmreu  32850  isopos  32921  islpln5  33275  islvol5  33319  pmapjat1  33593  dibelval3  34888  diblsmopel  34912  mapdpglem3  35416  hdmapglem7a  35671
  Copyright terms: Public domain W3C validator