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

Theorem exbid 1822
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 1810 . 2  |-  ( ph  ->  A. x ph )
3 exbid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3exbidh 1644 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  mobid  2282  rexbida  2844  rexeqf  3012  opabbid  4454  zfrepclf  4509  dfid3  4737  oprabbid  6240  axrepndlem1  8859  axrepndlem2  8860  axrepnd  8861  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem3  8867  axpowndlem3OLD  8868  axpowndlem4  8869  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axinfnd  8876  axacndlem4  8880  axacndlem5  8881  axacnd  8882  opabdm  26079  opabrn  26080  fpwrelmapffslem  26168  pm14.122b  29817  pm14.123b  29820
  Copyright terms: Public domain W3C validator