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

Theorem exbidv 1768
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 1758 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1727 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   E.wex 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem depends on definitions:  df-bi 189  df-ex 1664
This theorem is referenced by:  2exbidv  1770  3exbidv  1771  eubid  2317  eleq1d  2513  eleq2dALT  2516  rexbidv2  2897  ceqsex2  3086  alexeqg  3168  sbc2or  3276  sbc5  3292  sbcex2  3318  sbcabel  3345  elpreqprlem  4160  elpreqpr  4161  eluni  4201  csbuni  4226  intab  4265  cbvopab1  4473  cbvopab1s  4475  axrep1  4516  axrep2  4517  axrep3  4518  zfrepclf  4521  axsep2  4526  zfauscl  4527  euotd  4702  opeliunxp  4886  brcog  5001  elrn2g  5025  dfdmf  5028  eldmg  5030  dfrnf  5073  elrn2  5074  elrnmpt1  5083  brcodir  5219  dfco2a  5335  cores  5338  sbcfung  5605  brprcneu  5858  ssimaexg  5931  dmfco  5939  fndmdif  5986  fmptco  6056  fliftf  6208  cbvoprab1  6363  cbvoprab2  6364  snnex  6597  uniuni  6600  dmtpos  6985  wrecseq123  7029  wfrlem1  7035  wfrlem3a  7038  wfrlem15  7050  rdglim2  7150  ecdmn0  7406  mapsn  7513  bren  7578  brdomg  7579  domeng  7583  isinf  7785  ac6sfi  7815  ordiso  8031  brwdom  8082  brwdom2  8088  zfregcl  8109  inf0  8126  zfinf  8144  bnd2  8364  isinffi  8426  acneq  8474  acni  8476  aceq0  8549  aceq3lem  8551  dfac3  8552  dfac5lem4  8557  dfac8  8565  dfac9  8566  kmlem1  8580  kmlem2  8581  kmlem8  8587  kmlem10  8589  kmlem13  8592  cfval  8677  cardcf  8682  cfeq0  8686  cfsuc  8687  cff1  8688  cflim3  8692  cofsmo  8699  isfin4  8727  axcc2lem  8866  axcc4dom  8871  domtriomlem  8872  dcomex  8877  axdc2lem  8878  axdc4lem  8885  zfac  8890  ac7g  8904  ac4c  8906  ac5  8907  ac6sg  8918  weth  8925  axrepndlem1  9017  axunndlem1  9020  zfcndrep  9039  zfcndinf  9043  zfcndac  9044  gruina  9243  grothomex  9254  genpass  9434  1idpr  9454  ltexprlem3  9463  ltexprlem4  9464  ltexpri  9468  reclem2pr  9473  reclem3pr  9474  recexpr  9476  infm3  10568  nnunb  10865  axdc4uz  12196  ishashinf  12626  relexpindlem  13126  sumeq1  13755  sumeq2w  13758  sumeq2ii  13759  summo  13783  fsum  13786  fsum2dlem  13831  ntrivcvgn0  13954  ntrivcvgmullem  13957  prodeq1f  13962  prodeq2w  13966  prodeq2ii  13967  prodmo  13990  zprod  13991  fprod  13995  fprodntriv  13996  fprod2dlem  14034  ncoprmgcdne1b  14655  vdwapun  14924  vdwmc  14928  vdwmc2  14929  isacs  15557  dfiso2  15677  brssc  15719  isssc  15725  equivestrcsetc  16037  dirge  16483  gsumvalx  16513  gsumpropd  16515  gsumpropd2lem  16516  gsumress  16519  gsumval3eu  17538  gsumval3lem2  17540  dprd2d2  17677  znleval  19125  neitr  20196  cmpcovf  20406  hausmapdom  20515  ptval  20585  elpt  20587  ptpjopn  20627  ptclsg  20630  ptcnp  20637  uffix2  20939  cnextf  21081  prdsxmslem2  21544  metustfbas  21572  metcld2  22276  dchrmusumlema  24331  dchrisum0lema  24352  istrkgld  24507  uvtx01vtx  25220  wlkiswwlk2  25425  wlklniswwlkn2  25428  wlknwwlknvbij  25468  clwlkisclwwlk  25517  clwwlkvbij  25529  isgrpo  25924  ismgmOLD  26048  adjeu  27542  fcoinvbr  28215  fmptcof2  28259  acunirnmpt  28261  acunirnmpt2  28262  acunirnmpt2f  28263  aciunf1  28265  fpwrelmapffslem  28317  fmcncfil  28737  bnj865  29734  bnj1388  29842  bnj1489  29865  eldm3  30402  opelco3  30420  frrlem1  30514  elsingles  30685  funpartlem  30709  dfrdg4  30718  linedegen  30910  finminlem  30974  filnetlem4  31037  bj-axrep1  31403  bj-axrep2  31404  bj-axrep3  31405  bj-eleq1w  31455  bj-eleq2w  31456  bj-issetwt  31468  bj-ax8  31495  bj-axsep2  31528  bj-finsumval0  31702  csbwrecsg  31728  csboprabg  31731  topdifinffinlem  31750  wl-sb8eut  31906  sdclem1  32072  fdc  32074  isriscg  32223  islshpat  32583  lshpsmreu  32675  isopos  32746  islpln5  33100  islvol5  33144  pmapjat1  33418  dibelval3  34715  diblsmopel  34739  mapdpglem3  35243  hdmapglem7a  35498  dfac11  35920  clcnvlem  36230  dfhe3  36370  iotasbc  36770  iotasbc2  36771  sbcexgOLD  36904  csbunigOLD  37212  csbxpgOLD  37214  csbrngOLD  37217  fnchoice  37350  mapsnd  37476  mapsnend  37480  stoweidlem35  37896  stoweidlem39  37900  uvtxa01vtx0  39469  uspgrloopvd2  39557  opeliun2xp  40167
  Copyright terms: Public domain W3C validator