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

Theorem exbid 1789
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 1778 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1601 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1550   F/wnf 1553
This theorem is referenced by:  mobid  2314  rexbida  2712  rexeqf  2893  opabbid  4262  zfrepclf  4318  dfid3  4491  oprabbid  6119  axrepndlem1  8459  axrepndlem2  8460  axrepnd  8461  axpowndlem2  8465  axpowndlem3  8466  axpowndlem4  8467  axregnd  8471  axinfndlem1  8472  axinfnd  8473  axacndlem4  8477  axacndlem5  8478  axacnd  8479  pm14.122b  27591  pm14.123b  27594  drex2w3AUX7  29440  exdistrfNEW7  29442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator