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

Theorem exbidv 1679
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-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 1669 . 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 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669
This theorem depends on definitions:  df-bi 185  df-ex 1590
This theorem is referenced by:  2exbidv  1681  3exbidv  1682  eubid  2272  eleq1  2493  eleq2  2494  rexbidv2  2728  ceqsex2  2999  alexeqg  3077  alexeq  3078  sbc2or  3183  sbc5  3199  sbcex2  3228  sbcexgOLD  3229  sbcabel  3263  eluni  4082  csbuni  4107  csbunigOLD  4108  intab  4146  cbvopab1  4350  cbvopab1s  4352  axrep1  4392  axrep2  4393  axrep3  4394  zfrepclf  4397  axsep2  4402  zfauscl  4403  euotd  4580  opeliunxp  4877  csbxpgOLD  4906  brcog  4993  elrn2g  5017  dfdmf  5020  eldmg  5022  dfrnf  5065  elrn2  5066  elrnmpt1  5075  brcodir  5205  csbrngOLD  5288  dfco2a  5326  cores  5329  sbcfung  5429  brprcneu  5672  ssimaexg  5745  dmfco  5753  fndmdif  5795  fmptco  5863  fliftf  5995  cbvoprab1  6147  cbvoprab2  6148  snnex  6371  uniuni  6374  dmtpos  6746  rdglim2  6874  ecdmn0  7131  mapsn  7242  bren  7307  brdomg  7308  domeng  7312  isinf  7514  ac6sfi  7544  ordiso  7718  brwdom  7770  brwdom2  7776  zfregcl  7797  inf0  7815  zfinf  7833  bnd2  8088  isinffi  8150  acneq  8201  acni  8203  aceq0  8276  aceq3lem  8278  dfac3  8279  dfac5lem4  8284  dfac8  8292  dfac9  8293  kmlem1  8307  kmlem2  8308  kmlem8  8314  kmlem10  8316  kmlem13  8319  cfval  8404  cardcf  8409  cfeq0  8413  cfsuc  8414  cff1  8415  cflim3  8419  cofsmo  8426  isfin4  8454  axcc2lem  8593  axcc4dom  8598  domtriomlem  8599  dcomex  8604  axdc2lem  8605  axdc4lem  8612  zfac  8617  ac7g  8631  ac4c  8633  ac5  8634  ac6sg  8645  weth  8652  axrepndlem1  8744  axunndlem1  8747  zfcndrep  8769  zfcndinf  8773  zfcndac  8774  gruina  8973  grothomex  8984  genpass  9166  1idpr  9186  ltexprlem3  9195  ltexprlem4  9196  ltexpri  9200  reclem2pr  9205  reclem3pr  9206  recexpr  9208  infm3  10277  nnunb  10563  axdc4uz  11789  sumeq1  13150  sumeq2w  13153  sumeq2ii  13154  summo  13178  fsum  13181  fsum2dlem  13221  vdwapun  14018  vdwmc  14022  vdwmc2  14023  isacs  14572  brssc  14710  isssc  14716  dirge  15390  gsumvalx  15484  gsumpropd  15486  gsumress  15487  gsumval3eu  16361  gsumval3OLD  16362  gsumval3lem2  16364  dprd2d2  16517  znleval  17829  neitr  18626  cmpcovf  18836  hausmapdom  18946  ptval  18985  elpt  18987  ptpjopn  19027  ptclsg  19030  ptcnp  19037  uffix2  19339  cnextf  19480  prdsxmslem2  19946  metustfbasOLD  19982  metustfbas  19983  metcld2  20659  dchrmusumlema  22627  dchrisum0lema  22648  uvtx01vtx  23223  isgrpo  23506  ismgm  23630  adjeu  25116  fmptcof2  25803  ishashinf  25908  gsumpropd2lem  26093  fmcncfil  26215  relexpindlem  27188  ntrivcvgn0  27260  ntrivcvgmullem  27263  prodeq1f  27268  prodeq2w  27272  prodeq2ii  27273  prodmo  27296  zprod  27297  fprod  27301  fprodntriv  27302  fprod2dlem  27338  eldm3  27419  opelco3  27436  wrecseq123  27565  wfrlem1  27571  wfrlem15  27585  frrlem1  27615  elsingles  27796  funpartlem  27820  dfrdg4  27828  linedegen  28021  wl-sb8eut  28242  finminlem  28357  filnetlem4  28446  sdclem1  28483  fdc  28485  isriscg  28634  sbcom3OLD  28824  dfac11  29260  iotasbc  29518  iotasbc2  29519  fnchoice  29596  stoweidlem35  29676  stoweidlem39  29680  wlkiswwlk2  30177  wlklniswwlkn2  30180  wlknwwlknvbij  30218  clwlkisclwwlk  30297  clwwlkvbij  30309  opeliun2xp  30565  bnj865  31618  bnj1388  31726  bnj1489  31749  bj-axrep1  31929  bj-axrep2  31930  bj-axrep3  31931  bj-eleq1w  31970  bj-finsumval0  32159  islshpat  32235  lshpsmreu  32327  isopos  32398  islpln5  32752  islvol5  32796  pmapjat1  33070  dibelval3  34365  diblsmopel  34389  mapdpglem3  34893  hdmapglem7a  35148
  Copyright terms: Public domain W3C validator