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

Theorem exbidv 1637
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-17 1627 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1602 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   E.wex 1551
This theorem is referenced by:  2exbidv  1639  3exbidv  1640  eubid  2290  eleq1  2498  eleq2  2499  rexbidv2  2730  ceqsex2  2994  alexeq  3067  ceqex  3068  sbc2or  3171  sbc5  3187  sbcex2  3212  sbcexg  3213  sbcabel  3240  eluni  4020  csbunig  4025  intab  4082  cbvopab1  4280  cbvopab1s  4282  axrep1  4323  axrep2  4324  axrep3  4325  zfrepclf  4328  axsep2  4333  zfauscl  4334  euotd  4459  snnex  4715  uniuni  4718  csbxpg  4907  opeliunxp  4931  brcog  5041  elrn2g  5063  dfdmf  5066  eldmg  5067  dfrnf  5110  elrn2  5111  csbrng  5116  elrnmpt1  5121  brcodir  5255  dfco2a  5372  cores  5375  brprcneu  5723  ssimaexg  5791  dmfco  5799  fndmdif  5836  fmptco  5903  fliftf  6039  cbvoprab1  6146  cbvoprab2  6147  dmtpos  6493  rdglim2  6692  ecdmn0  6949  mapsn  7057  bren  7119  brdomg  7120  domeng  7124  isinf  7324  ac6sfi  7353  ordiso  7487  brwdom  7537  brwdom2  7543  zfregcl  7564  inf0  7578  zfinf  7596  bnd2  7819  isinffi  7881  acneq  7926  acni  7928  aceq0  8001  aceq3lem  8003  dfac3  8004  dfac5lem4  8009  dfac8  8017  dfac9  8018  kmlem1  8032  kmlem2  8033  kmlem8  8039  kmlem10  8041  kmlem13  8044  cfval  8129  cardcf  8134  cfeq0  8138  cfsuc  8139  cff1  8140  cflim3  8144  cofsmo  8151  isfin4  8179  axcc2lem  8318  axcc4dom  8323  domtriomlem  8324  dcomex  8329  axdc2lem  8330  axdc4lem  8337  zfac  8342  ac7g  8356  ac4c  8358  ac5  8359  ac6sg  8370  weth  8377  axrepndlem1  8469  axunndlem1  8472  zfcndrep  8491  zfcndinf  8495  zfcndac  8496  gruina  8695  grothomex  8706  genpass  8888  1idpr  8908  ltexprlem3  8917  ltexprlem4  8918  ltexpri  8922  reclem2pr  8927  reclem3pr  8928  recexpr  8930  infm3  9969  nnunb  10219  axdc4uz  11324  sumeq1f  12484  sumeq2w  12488  sumeq2ii  12489  cbvsum  12491  summo  12513  fsum  12516  fsum2dlem  12556  vdwapun  13344  vdwmc  13348  vdwmc2  13349  isacs  13878  brssc  14016  isssc  14022  dirge  14684  gsumvalx  14776  gsumpropd  14778  gsumress  14779  gsumval3eu  15515  gsumval3  15516  dprd2d2  15604  znleval  16837  neitr  17246  cmpcovf  17456  hausmapdom  17565  ptval  17604  elpt  17606  ptpjopn  17646  ptclsg  17649  ptcnp  17656  uffix2  17958  cnextf  18099  prdsxmslem2  18561  metustfbasOLD  18597  metustfbas  18598  metcld2  19261  dchrmusumlema  21189  dchrisum0lema  21210  uvtx01vtx  21503  isgrpo  21786  ismgm  21910  adjeu  23394  fmptcof2  24078  ishashinf  24161  gsumpropd2lem  24222  fmcncfil  24319  relexpindlem  25141  ntrivcvgn0  25228  ntrivcvgmullem  25231  prodeq1f  25236  prodeq2w  25240  prodeq2ii  25241  prodmo  25264  zprod  25265  fprod  25269  fprodntriv  25270  fprod2dlem  25306  eldm3  25387  opelco3  25405  wrecseq123  25534  wfrlem1  25540  wfrlem15  25554  frrlem1  25584  elsingles  25765  funpartlem  25789  dfrdg4  25797  linedegen  26079  finminlem  26323  filnetlem4  26412  sdclem1  26449  fdc  26451  isriscg  26602  dfac11  27139  iotasbc  27598  iotasbc2  27599  fnchoice  27678  stoweidlem35  27762  stoweidlem39  27766  csbdmg  27960  sbcfun  27965  wlkiswwlk2  28367  wlklniswwlkn2  28370  bnj865  29356  bnj1388  29464  bnj1489  29487  islshpat  29877  lshpsmreu  29969  isopos  30040  islpln5  30394  islvol5  30438  pmapjat1  30712  dibelval3  32007  diblsmopel  32031  mapdpglem3  32535  hdmapglem7a  32790
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator