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

Theorem exbid 1939
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 1927 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1723 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E.wex 1659   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664
This theorem is referenced by:  mobid  2287  rexbida  2941  rexeqf  3029  opabbid  4488  zfrepclf  4544  dfid3  4770  oprabbid  6358  axrepndlem1  9015  axrepndlem2  9016  axrepnd  9017  axpowndlem2  9021  axpowndlem3  9022  axpowndlem4  9023  axregnd  9027  axregndOLD  9028  axinfndlem1  9029  axinfnd  9030  axacndlem4  9034  axacndlem5  9035  axacnd  9036  opabdm  28066  opabrn  28067  pm14.122b  36426  pm14.123b  36429
  Copyright terms: Public domain W3C validator