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

Theorem exbidv 1722
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 1712 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1684 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-ex 1621
This theorem is referenced by:  2exbidv  1724  3exbidv  1725  eubid  2238  eleq1d  2451  eleq2dALT  2453  eleq1OLD  2456  eleq2OLD  2457  rexbidv2  2889  ceqsex2  3072  alexeqg  3153  alexeq  3154  sbc2or  3261  sbc5  3277  sbcex2  3303  sbcabel  3330  eluni  4166  csbuni  4191  intab  4230  cbvopab1  4437  cbvopab1s  4439  axrep1  4479  axrep2  4480  axrep3  4481  zfrepclf  4484  axsep2  4489  zfauscl  4490  euotd  4662  opeliunxp  4965  brcog  5082  elrn2g  5106  dfdmf  5109  eldmg  5111  dfrnf  5154  elrn2  5155  elrnmpt1  5164  brcodir  5299  dfco2a  5415  cores  5418  sbcfung  5519  brprcneu  5767  ssimaexg  5840  dmfco  5848  fndmdif  5893  fmptco  5966  fliftf  6114  cbvoprab1  6268  cbvoprab2  6269  snnex  6505  uniuni  6508  dmtpos  6885  rdglim2  7016  ecdmn0  7272  mapsn  7379  bren  7444  brdomg  7445  domeng  7449  isinf  7649  ac6sfi  7679  ordiso  7856  brwdom  7908  brwdom2  7914  zfregcl  7935  inf0  7952  zfinf  7970  bnd2  8224  isinffi  8286  acneq  8337  acni  8339  aceq0  8412  aceq3lem  8414  dfac3  8415  dfac5lem4  8420  dfac8  8428  dfac9  8429  kmlem1  8443  kmlem2  8444  kmlem8  8450  kmlem10  8452  kmlem13  8455  cfval  8540  cardcf  8545  cfeq0  8549  cfsuc  8550  cff1  8551  cflim3  8555  cofsmo  8562  isfin4  8590  axcc2lem  8729  axcc4dom  8734  domtriomlem  8735  dcomex  8740  axdc2lem  8741  axdc4lem  8748  zfac  8753  ac7g  8767  ac4c  8769  ac5  8770  ac6sg  8781  weth  8788  axrepndlem1  8880  axunndlem1  8883  zfcndrep  8903  zfcndinf  8907  zfcndac  8908  gruina  9107  grothomex  9118  genpass  9298  1idpr  9318  ltexprlem3  9327  ltexprlem4  9328  ltexpri  9332  reclem2pr  9337  reclem3pr  9338  recexpr  9340  infm3  10418  nnunb  10708  axdc4uz  11996  relexpindlem  12898  sumeq1  13513  sumeq2w  13516  sumeq2ii  13517  summo  13541  fsum  13544  fsum2dlem  13587  ntrivcvgn0  13709  ntrivcvgmullem  13712  prodeq1f  13717  prodeq2w  13721  prodeq2ii  13722  prodmo  13745  zprod  13746  fprod  13750  fprodntriv  13751  fprod2dlem  13786  vdwapun  14494  vdwmc  14498  vdwmc2  14499  isacs  15058  dfiso2  15178  brssc  15220  isssc  15226  equivestrcsetc  15538  dirge  15984  gsumvalx  16014  gsumpropd  16016  gsumpropd2lem  16017  gsumress  16020  gsumval3eu  17024  gsumval3OLD  17025  gsumval3lem2  17027  dprd2d2  17206  znleval  18684  neitr  19767  cmpcovf  19977  hausmapdom  20086  ptval  20156  elpt  20158  ptpjopn  20198  ptclsg  20201  ptcnp  20208  uffix2  20510  cnextf  20651  prdsxmslem2  21117  metustfbasOLD  21153  metustfbas  21154  metcld2  21830  dchrmusumlema  23795  dchrisum0lema  23816  istrkgld  23974  uvtx01vtx  24613  wlkiswwlk2  24818  wlklniswwlkn2  24821  wlknwwlknvbij  24861  clwlkisclwwlk  24910  clwwlkvbij  24922  isgrpo  25315  ismgmOLD  25439  adjeu  26924  fcoinvbr  27594  fmptcof2  27643  acunirnmpt  27645  acunirnmpt2  27646  acunirnmpt2f  27647  aciunf1  27649  fpwrelmapffslem  27705  ishashinf  27759  fmcncfil  28067  eldm3  29357  opelco3  29373  wrecseq123  29502  wfrlem1  29508  wfrlem15  29522  frrlem1  29552  elsingles  29721  funpartlem  29745  dfrdg4  29753  linedegen  29946  wl-sb8eut  30187  finminlem  30302  filnetlem4  30365  sdclem1  30402  fdc  30404  isriscg  30553  dfac11  31174  iotasbc  31494  iotasbc2  31495  fnchoice  31571  stoweidlem35  31983  stoweidlem39  31987  opeliun2xp  33122  sbcexgOLD  33650  csbunigOLD  33962  csbxpgOLD  33964  csbrngOLD  33967  bnj865  34328  bnj1388  34436  bnj1489  34459  bj-axrep1  34721  bj-axrep2  34722  bj-axrep3  34723  bj-eleq1w  34769  bj-eleq2w  34770  bj-issetwt  34782  bj-axsep2  34840  bj-finsumval0  35010  islshpat  35155  lshpsmreu  35247  isopos  35318  islpln5  35672  islvol5  35716  pmapjat1  35990  dibelval3  37287  diblsmopel  37311  mapdpglem3  37815  hdmapglem7a  38070  dfhe3  38269
  Copyright terms: Public domain W3C validator