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

Theorem exbidv 1633
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 1623 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1598 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547
This theorem is referenced by:  2exbidv  1635  3exbidv  1636  eubid  2261  eleq1  2464  eleq2  2465  rexbidv2  2689  ceqsex2  2952  alexeq  3025  ceqex  3026  sbc2or  3129  sbc5  3145  sbcex2  3170  sbcexg  3171  sbcabel  3198  eluni  3978  csbunig  3983  intab  4040  cbvopab1  4238  cbvopab1s  4240  axrep1  4281  axrep2  4282  axrep3  4283  zfrepclf  4286  axsep2  4291  zfauscl  4292  euotd  4417  snnex  4672  uniuni  4675  csbxpg  4864  opeliunxp  4888  brcog  4998  elrn2g  5020  dfdmf  5023  eldmg  5024  dfrnf  5067  elrn2  5068  csbrng  5073  elrnmpt1  5078  brcodir  5212  dfco2a  5329  cores  5332  brprcneu  5680  ssimaexg  5748  dmfco  5756  fndmdif  5793  fmptco  5860  fliftf  5996  cbvoprab1  6103  cbvoprab2  6104  dmtpos  6450  rdglim2  6649  ecdmn0  6906  mapsn  7014  bren  7076  brdomg  7077  domeng  7081  isinf  7281  ac6sfi  7310  ordiso  7441  brwdom  7491  brwdom2  7497  zfregcl  7518  inf0  7532  zfinf  7550  bnd2  7773  isinffi  7835  acneq  7880  acni  7882  aceq0  7955  aceq3lem  7957  dfac3  7958  dfac5lem4  7963  dfac8  7971  dfac9  7972  kmlem1  7986  kmlem2  7987  kmlem8  7993  kmlem10  7995  kmlem13  7998  cfval  8083  cardcf  8088  cfeq0  8092  cfsuc  8093  cff1  8094  cflim3  8098  cofsmo  8105  isfin4  8133  axcc2lem  8272  axcc4dom  8277  domtriomlem  8278  dcomex  8283  axdc2lem  8284  axdc4lem  8291  zfac  8296  ac7g  8310  ac4c  8312  ac5  8313  ac6sg  8324  weth  8331  axrepndlem1  8423  axunndlem1  8426  zfcndrep  8445  zfcndinf  8449  zfcndac  8450  gruina  8649  grothomex  8660  genpass  8842  1idpr  8862  ltexprlem3  8871  ltexprlem4  8872  ltexpri  8876  reclem2pr  8881  reclem3pr  8882  recexpr  8884  infm3  9923  nnunb  10173  axdc4uz  11277  sumeq1f  12437  sumeq2w  12441  sumeq2ii  12442  cbvsum  12444  summo  12466  fsum  12469  fsum2dlem  12509  vdwapun  13297  vdwmc  13301  vdwmc2  13302  isacs  13831  brssc  13969  isssc  13975  dirge  14637  gsumvalx  14729  gsumpropd  14731  gsumress  14732  gsumval3eu  15468  gsumval3  15469  dprd2d2  15557  znleval  16790  neitr  17198  cmpcovf  17408  hausmapdom  17516  ptval  17555  elpt  17557  ptpjopn  17597  ptclsg  17600  ptcnp  17607  uffix2  17909  cnextf  18050  prdsxmslem2  18512  metustfbasOLD  18548  metustfbas  18549  metcld2  19212  dchrmusumlema  21140  dchrisum0lema  21161  uvtx01vtx  21454  isgrpo  21737  ismgm  21861  adjeu  23345  fmptcof2  24029  ishashinf  24112  gsumpropd2lem  24173  fmcncfil  24270  relexpindlem  25092  ntrivcvgn0  25179  ntrivcvgmullem  25182  prodeq1f  25187  prodeq2w  25191  prodeq2ii  25192  prodmo  25215  zprod  25216  fprod  25220  fprodntriv  25221  fprod2dlem  25257  eldm3  25333  wfrlem1  25470  wfrlem15  25484  frrlem1  25495  elsingles  25671  brimg  25690  funpartlem  25695  dfrdg4  25703  linedegen  25981  bpolylem  25998  bpolyval  25999  finminlem  26211  filnetlem4  26300  sdclem1  26337  fdc  26339  isriscg  26490  dfac11  27028  iotasbc  27487  iotasbc2  27488  fnchoice  27567  stoweidlem35  27651  stoweidlem39  27655  csbdmg  27849  sbcfun  27854  bnj865  29000  bnj1388  29108  bnj1489  29131  islshpat  29500  lshpsmreu  29592  isopos  29663  islpln5  30017  islvol5  30061  pmapjat1  30335  dibelval3  31630  diblsmopel  31654  mapdpglem3  32158  hdmapglem7a  32413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator