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

Theorem exbid 2216
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 2188 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1870 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wex 1781  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfbidf  2217  drex2  2441  rexbida  3269  rexeqfOLD  3351  opabbid  5213  zfrepclf  5294  dfid3  5577  oprabbid  7473  axrepndlem1  10586  axrepndlem2  10587  axrepnd  10588  axpowndlem2  10592  axpowndlem3  10593  axpowndlem4  10594  axregnd  10598  axinfndlem1  10599  axinfnd  10600  axacndlem4  10604  axacndlem5  10605  axacnd  10606  opabdm  31835  opabrn  31836  pm14.122b  43172  pm14.123b  43175
  Copyright terms: Public domain W3C validator