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

Theorem exbid 2258
Description: Formula-building rule for existential quantifier (deduction rule). (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 2229 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1955 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wex 1859  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-12 2213
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864
This theorem is referenced by:  nfbidf  2259  drex2  2489  mobid  2648  rexbida  3231  rexeqf  3320  opabbid  4902  zfrepclf  4964  dfid3  5214  oprabbid  6932  axrepndlem1  9693  axrepndlem2  9694  axrepnd  9695  axpowndlem2  9699  axpowndlem3  9700  axpowndlem4  9701  axregnd  9705  axinfndlem1  9706  axinfnd  9707  axacndlem4  9711  axacndlem5  9712  axacnd  9713  opabdm  29742  opabrn  29743  pm14.122b  39117  pm14.123b  39120
  Copyright terms: Public domain W3C validator