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

Theorem exbid 2211
Description: Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
albid.1 𝑥𝜑
albid.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exbid (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Proof of Theorem exbid
StepHypRef Expression
1 albid.1 . . 3 𝑥𝜑
21nf5ri 2183 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1862 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wex 1773  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778
This theorem is referenced by:  nfbidf  2212  drex2  2435  rexbida  3259  rexeqfOLD  3338  opabbid  5214  zfrepclf  5295  dfid3  5579  oprabbid  7485  axrepndlem1  10622  axrepndlem2  10623  axrepnd  10624  axpowndlem2  10628  axpowndlem3  10629  axpowndlem4  10630  axregnd  10634  axinfndlem1  10635  axinfnd  10636  axacndlem4  10640  axacndlem5  10641  axacnd  10642  opabdm  32500  opabrn  32501  pm14.122b  44007  pm14.123b  44010
  Copyright terms: Public domain W3C validator