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

Theorem exbid 1765
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 1754 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1581 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1531   F/wnf 1534
This theorem is referenced by:  mobid  2190  rexbida  2571  rexeqf  2746  opabbid  4097  zfrepclf  4153  dfid3  4326  oprabbid  5917  axrepndlem1  8230  axrepndlem2  8231  axrepnd  8232  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axregnd  8242  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  fmptcof2  23244  pm14.122b  27726  pm14.123b  27729  drex2w3AUX7  29480  exdistrfNEW7  29482
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  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator