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

Theorem exbid 1964
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 1952 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1727 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   E.wex 1663   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668
This theorem is referenced by:  mobid  2318  rexbida  2896  rexeqf  2984  opabbid  4465  zfrepclf  4521  dfid3  4750  oprabbid  6344  axrepndlem1  9017  axrepndlem2  9018  axrepnd  9019  axpowndlem2  9023  axpowndlem3  9024  axpowndlem4  9025  axregnd  9029  axinfndlem1  9030  axinfnd  9031  axacndlem4  9035  axacndlem5  9036  axacnd  9037  opabdm  28219  opabrn  28220  pm14.122b  36774  pm14.123b  36777
  Copyright terms: Public domain W3C validator