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

Theorem exbid 1753
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 1742 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1578 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1528   F/wnf 1531
This theorem is referenced by:  mobid  2177  rexbida  2558  rexeqf  2733  opabbid  4081  zfrepclf  4137  dfid3  4310  oprabbid  5901  axrepndlem1  8214  axrepndlem2  8215  axrepnd  8216  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  fmptcof2  23229  pm14.122b  27623  pm14.123b  27626
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator