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

Theorem exbidv 1701
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 1691 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1663 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-ex 1600
This theorem is referenced by:  2exbidv  1703  3exbidv  1704  eubid  2288  eleq1d  2512  eleq2dALT  2514  eleq1OLD  2517  eleq2OLD  2518  rexbidv2  2950  ceqsex2  3133  alexeqg  3214  alexeq  3215  sbc2or  3322  sbc5  3338  sbcex2  3367  sbcexgOLD  3368  sbcabel  3402  eluni  4237  csbuni  4262  csbunigOLD  4263  intab  4302  cbvopab1  4507  cbvopab1s  4509  axrep1  4549  axrep2  4550  axrep3  4551  zfrepclf  4554  axsep2  4559  zfauscl  4560  euotd  4738  opeliunxp  5041  csbxpgOLD  5072  brcog  5159  elrn2g  5183  dfdmf  5186  eldmg  5188  dfrnf  5231  elrn2  5232  elrnmpt1  5241  brcodir  5376  csbrngOLD  5459  dfco2a  5497  cores  5500  sbcfung  5601  brprcneu  5849  ssimaexg  5924  dmfco  5932  fndmdif  5976  fmptco  6049  fliftf  6198  cbvoprab1  6354  cbvoprab2  6355  snnex  6591  uniuni  6594  dmtpos  6969  rdglim2  7100  ecdmn0  7356  mapsn  7462  bren  7527  brdomg  7528  domeng  7532  isinf  7735  ac6sfi  7766  ordiso  7944  brwdom  7996  brwdom2  8002  zfregcl  8023  inf0  8041  zfinf  8059  bnd2  8314  isinffi  8376  acneq  8427  acni  8429  aceq0  8502  aceq3lem  8504  dfac3  8505  dfac5lem4  8510  dfac8  8518  dfac9  8519  kmlem1  8533  kmlem2  8534  kmlem8  8540  kmlem10  8542  kmlem13  8545  cfval  8630  cardcf  8635  cfeq0  8639  cfsuc  8640  cff1  8641  cflim3  8645  cofsmo  8652  isfin4  8680  axcc2lem  8819  axcc4dom  8824  domtriomlem  8825  dcomex  8830  axdc2lem  8831  axdc4lem  8838  zfac  8843  ac7g  8857  ac4c  8859  ac5  8860  ac6sg  8871  weth  8878  axrepndlem1  8970  axunndlem1  8973  zfcndrep  8995  zfcndinf  8999  zfcndac  9000  gruina  9199  grothomex  9210  genpass  9390  1idpr  9410  ltexprlem3  9419  ltexprlem4  9420  ltexpri  9424  reclem2pr  9429  reclem3pr  9430  recexpr  9432  infm3  10508  nnunb  10797  axdc4uz  12072  sumeq1  13490  sumeq2w  13493  sumeq2ii  13494  summo  13518  fsum  13521  fsum2dlem  13564  vdwapun  14369  vdwmc  14373  vdwmc2  14374  isacs  14925  brssc  15060  isssc  15066  dirge  15741  gsumvalx  15771  gsumpropd  15773  gsumpropd2lem  15774  gsumress  15777  gsumval3eu  16781  gsumval3OLD  16782  gsumval3lem2  16784  dprd2d2  16967  znleval  18466  neitr  19554  cmpcovf  19764  hausmapdom  19874  ptval  19944  elpt  19946  ptpjopn  19986  ptclsg  19989  ptcnp  19996  uffix2  20298  cnextf  20439  prdsxmslem2  20905  metustfbasOLD  20941  metustfbas  20942  metcld2  21618  dchrmusumlema  23550  dchrisum0lema  23571  istrkgld  23729  uvtx01vtx  24364  wlkiswwlk2  24569  wlklniswwlkn2  24572  wlknwwlknvbij  24612  clwlkisclwwlk  24661  clwwlkvbij  24673  isgrpo  25070  ismgmOLD  25194  adjeu  26680  fcoinvbr  27333  fmptcof2  27374  fpwrelmapffslem  27427  ishashinf  27478  fmcncfil  27786  relexpindlem  28935  ntrivcvgn0  29007  ntrivcvgmullem  29010  prodeq1f  29015  prodeq2w  29019  prodeq2ii  29020  prodmo  29043  zprod  29044  fprod  29048  fprodntriv  29049  fprod2dlem  29085  eldm3  29166  opelco3  29183  wrecseq123  29312  wfrlem1  29318  wfrlem15  29332  frrlem1  29362  elsingles  29543  funpartlem  29567  dfrdg4  29575  linedegen  29768  wl-sb8eut  29997  finminlem  30111  filnetlem4  30174  sdclem1  30211  fdc  30213  isriscg  30362  dfac11  30983  iotasbc  31280  iotasbc2  31281  fnchoice  31358  stoweidlem35  31706  stoweidlem39  31710  opeliun2xp  32655  bnj865  33714  bnj1388  33822  bnj1489  33845  bj-axrep1  34122  bj-axrep2  34123  bj-axrep3  34124  bj-eleq1w  34170  bj-eleq2w  34171  bj-issetwt  34183  bj-axsep2  34241  bj-finsumval0  34403  islshpat  34482  lshpsmreu  34574  isopos  34645  islpln5  34999  islvol5  35043  pmapjat1  35317  dibelval3  36614  diblsmopel  36638  mapdpglem3  37142  hdmapglem7a  37397  dfhe3  37486
  Copyright terms: Public domain W3C validator