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

Theorem exbidv 1616
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 1606 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1581 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1531
This theorem is referenced by:  2exbidv  1618  3exbidv  1619  eubid  2163  eleq1  2356  eleq2  2357  rexbidv2  2579  ceqsex2  2837  alexeq  2910  ceqex  2911  sbc2or  3012  sbc5  3028  sbcex2  3053  sbcexg  3054  sbcabel  3081  eluni  3846  csbunig  3851  intab  3908  cbvopab1  4105  cbvopab1s  4107  axrep1  4148  axrep2  4149  axrep3  4150  zfrepclf  4153  axsep2  4158  zfauscl  4159  euotd  4283  snnex  4540  uniuni  4543  csbxpg  4732  opeliunxp  4756  brcog  4866  elrn2g  4886  dfdmf  4889  eldmg  4890  dfrnf  4933  elrn2  4934  csbrng  4939  elrnmpt1  4944  brcodir  5078  dfco2a  5189  cores  5192  brprcneu  5534  ssimaexg  5601  dmfco  5609  fndmdif  5645  fmptco  5707  fliftf  5830  cbvoprab1  5934  cbvoprab2  5935  dmtpos  6262  rdglim2  6461  ecdmn0  6718  mapsn  6825  bren  6887  brdomg  6888  domeng  6892  isinf  7092  ac6sfi  7117  ordiso  7247  brwdom  7297  brwdom2  7303  zfregcl  7324  inf0  7338  zfinf  7356  bnd2  7579  isinffi  7641  acneq  7686  acni  7688  aceq0  7761  aceq3lem  7763  dfac3  7764  dfac5lem4  7769  dfac8  7777  dfac9  7778  kmlem1  7792  kmlem2  7793  kmlem8  7799  kmlem10  7801  kmlem13  7804  cfval  7889  cardcf  7894  cfeq0  7898  cfsuc  7899  cff1  7900  cflim3  7904  cofsmo  7911  isfin4  7939  axcc2lem  8078  axcc4dom  8083  domtriomlem  8084  dcomex  8089  axdc2lem  8090  axdc4lem  8097  zfac  8102  ac7g  8117  ac4c  8119  ac5  8120  ac6sg  8131  weth  8138  axrepndlem1  8230  axunndlem1  8233  zfcndrep  8252  zfcndinf  8256  zfcndac  8257  gruina  8456  grothomex  8467  genpass  8649  1idpr  8669  ltexprlem3  8678  ltexprlem4  8679  ltexpri  8683  reclem2pr  8688  reclem3pr  8689  recexpr  8691  infm3  9729  nnunb  9977  axdc4uz  11061  sumeq1f  12177  sumeq2w  12181  sumeq2ii  12182  cbvsum  12184  summo  12206  fsum  12209  fsum2dlem  12249  vdwapun  13037  vdwmc  13041  vdwmc2  13042  isacs  13569  brssc  13707  isssc  13713  dirge  14375  gsumvalx  14467  gsumpropd  14469  gsumress  14470  gsumval3eu  15206  gsumval3  15207  dprd2d2  15295  znleval  16524  cmpcovf  17134  hausmapdom  17242  ptval  17281  elpt  17283  ptpjopn  17322  ptclsg  17325  ptcnp  17332  uffix2  17635  prdsxmslem2  18091  metcld2  18748  dchrmusumlema  20658  dchrisum0lema  20679  isgrpo  20879  ismgm  21003  adjeu  22485  gsumpropd2lem  23394  ishashinf  23404  itgmeq123dTMP  23604  relexpindlem  24051  cprodeq1f  24130  cprodeq2w  24134  cprodeq2ii  24135  prodmo  24159  zprod  24160  zprodn0  24162  fprod  24164  eldm3  24190  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  elsingles  24528  brimg  24547  funpartlem  24552  dfrdg4  24560  linedegen  24838  bpolylem  24855  bpolyval  24856  itg2addnc  25005  alexeqd  25065  copsexgb  25069  ac5g  25178  surjsec2  25223  islatalg  25286  prodeq1  25409  prodeq2  25410  prodeq3ii  25411  fisub  25657  finminlem  26334  filnetlem4  26433  sdclem1  26556  fdc  26558  isriscg  26718  dfac11  27263  iotasbc  27722  iotasbc2  27723  fnchoice  27803  stoweidlem35  27887  stoweidlem39  27891  csbdmg  28085  sbcfun  28090  uvtx01vtx  28305  bnj865  29271  bnj1388  29379  bnj1489  29402  islshpat  29829  lshpsmreu  29921  isopos  29992  islpln5  30346  islvol5  30390  pmapjat1  30664  dibelval3  31959  diblsmopel  31983  mapdpglem3  32487  hdmapglem7a  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator