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

Theorem exbid 1984
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 1972 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1735 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   E.wex 1671   F/wnf 1675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676
This theorem is referenced by:  mobid  2338  rexbida  2887  rexeqf  2970  opabbid  4458  zfrepclf  4514  dfid3  4755  oprabbid  6363  axrepndlem1  9035  axrepndlem2  9036  axrepnd  9037  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axregnd  9047  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  opabdm  28295  opabrn  28296  pm14.122b  36844  pm14.123b  36847
  Copyright terms: Public domain W3C validator