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

Theorem exbidv 1761
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 1751 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1723 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  2exbidv  1763  3exbidv  1764  eubid  2286  eleq1d  2498  eleq2dALT  2500  eleq1OLD  2503  eleq2OLD  2504  rexbidv2  2942  ceqsex2  3125  alexeqg  3206  alexeq  3207  sbc2or  3314  sbc5  3330  sbcex2  3356  sbcabel  3383  eluni  4225  csbuni  4250  intab  4289  cbvopab1  4496  cbvopab1s  4498  axrep1  4539  axrep2  4540  axrep3  4541  zfrepclf  4544  axsep2  4549  zfauscl  4550  euotd  4722  opeliunxp  4906  brcog  5021  elrn2g  5045  dfdmf  5048  eldmg  5050  dfrnf  5093  elrn2  5094  elrnmpt1  5103  brcodir  5239  dfco2a  5355  cores  5358  sbcfung  5624  brprcneu  5874  ssimaexg  5947  dmfco  5955  fndmdif  6001  fmptco  6071  fliftf  6223  cbvoprab1  6377  cbvoprab2  6378  snnex  6611  uniuni  6614  dmtpos  6993  wrecseq123  7037  wfrlem1  7043  wfrlem3a  7046  wfrlem15  7058  rdglim2  7158  ecdmn0  7414  mapsn  7521  bren  7586  brdomg  7587  domeng  7591  isinf  7791  ac6sfi  7821  ordiso  8031  brwdom  8082  brwdom2  8088  zfregcl  8109  inf0  8126  zfinf  8144  bnd2  8363  isinffi  8425  acneq  8472  acni  8474  aceq0  8547  aceq3lem  8549  dfac3  8550  dfac5lem4  8555  dfac8  8563  dfac9  8564  kmlem1  8578  kmlem2  8579  kmlem8  8585  kmlem10  8587  kmlem13  8590  cfval  8675  cardcf  8680  cfeq0  8684  cfsuc  8685  cff1  8686  cflim3  8690  cofsmo  8697  isfin4  8725  axcc2lem  8864  axcc4dom  8869  domtriomlem  8870  dcomex  8875  axdc2lem  8876  axdc4lem  8883  zfac  8888  ac7g  8902  ac4c  8904  ac5  8905  ac6sg  8916  weth  8923  axrepndlem1  9015  axunndlem1  9018  zfcndrep  9038  zfcndinf  9042  zfcndac  9043  gruina  9242  grothomex  9253  genpass  9433  1idpr  9453  ltexprlem3  9462  ltexprlem4  9463  ltexpri  9467  reclem2pr  9472  reclem3pr  9473  recexpr  9475  infm3  10568  nnunb  10865  axdc4uz  12193  relexpindlem  13105  sumeq1  13733  sumeq2w  13736  sumeq2ii  13737  summo  13761  fsum  13764  fsum2dlem  13809  ntrivcvgn0  13932  ntrivcvgmullem  13935  prodeq1f  13940  prodeq2w  13944  prodeq2ii  13945  prodmo  13968  zprod  13969  fprod  13973  fprodntriv  13974  fprod2dlem  14012  ncoprmgcdne1b  14617  vdwapun  14878  vdwmc  14882  vdwmc2  14883  isacs  15499  dfiso2  15619  brssc  15661  isssc  15667  equivestrcsetc  15979  dirge  16425  gsumvalx  16455  gsumpropd  16457  gsumpropd2lem  16458  gsumress  16461  gsumval3eu  17464  gsumval3lem2  17466  dprd2d2  17603  znleval  19047  neitr  20118  cmpcovf  20328  hausmapdom  20437  ptval  20507  elpt  20509  ptpjopn  20549  ptclsg  20552  ptcnp  20559  uffix2  20861  cnextf  21003  prdsxmslem2  21466  metustfbas  21494  metcld2  22160  dchrmusumlema  24185  dchrisum0lema  24206  istrkgld  24361  uvtx01vtx  25056  wlkiswwlk2  25261  wlklniswwlkn2  25264  wlknwwlknvbij  25304  clwlkisclwwlk  25353  clwwlkvbij  25365  isgrpo  25760  ismgmOLD  25884  adjeu  27368  fcoinvbr  28045  fmptcof2  28090  acunirnmpt  28092  acunirnmpt2  28093  acunirnmpt2f  28094  aciunf1  28096  fpwrelmapffslem  28151  ishashinf  28208  fmcncfil  28567  bnj865  29513  bnj1388  29621  bnj1489  29644  eldm3  30180  opelco3  30198  frrlem1  30292  elsingles  30461  funpartlem  30485  dfrdg4  30494  linedegen  30686  finminlem  30750  filnetlem4  30813  bj-axrep1  31145  bj-axrep2  31146  bj-axrep3  31147  bj-eleq1w  31197  bj-eleq2w  31198  bj-issetwt  31210  bj-ax8  31236  bj-axsep2  31269  bj-finsumval0  31438  topdifinffinlem  31475  wl-sb8eut  31600  sdclem1  31766  fdc  31768  isriscg  31917  islshpat  32282  lshpsmreu  32374  isopos  32445  islpln5  32799  islvol5  32843  pmapjat1  33117  dibelval3  34414  diblsmopel  34438  mapdpglem3  34942  hdmapglem7a  35197  dfac11  35616  dfhe3  35997  iotasbc  36397  iotasbc2  36398  sbcexgOLD  36531  csbunigOLD  36842  csbxpgOLD  36844  csbrngOLD  36847  fnchoice  36980  stoweidlem35  37455  stoweidlem39  37459  opeliun2xp  38864
  Copyright terms: Public domain W3C validator