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

Theorem exbid 1781
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exbid.1  |-  F/ x ph
exbid.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
exbid  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )

Proof of Theorem exbid
StepHypRef Expression
1 exbid.1 . . 3  |-  F/ x ph
21nfri 1770 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1598 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547   F/wnf 1550
This theorem is referenced by:  mobid  2265  rexbida  2657  rexeqf  2837  opabbid  4204  zfrepclf  4260  dfid3  4433  oprabbid  6059  axrepndlem1  8393  axrepndlem2  8394  axrepnd  8395  axpowndlem2  8399  axpowndlem3  8400  axpowndlem4  8401  axregnd  8405  axinfndlem1  8406  axinfnd  8407  axacndlem4  8411  axacndlem5  8412  axacnd  8413  pm14.122b  27285  pm14.123b  27288  drex2w3AUX7  28834  exdistrfNEW7  28836
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  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator