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

Theorem exbid 2266
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 2236 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1968 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wex 1878  wnf 1882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-12 2220
This theorem depends on definitions:  df-bi 199  df-ex 1879  df-nf 1883
This theorem is referenced by:  nfbidf  2267  drex2  2463  eubidOLD  2661  mobidOLDOLD  2681  rexbida  3257  rexeqf  3347  opabbid  4940  zfrepclf  5003  dfid3  5253  oprabbid  6973  axrepndlem1  9736  axrepndlem2  9737  axrepnd  9738  axpowndlem2  9742  axpowndlem3  9743  axpowndlem4  9744  axregnd  9748  axinfndlem1  9749  axinfnd  9750  axacndlem4  9754  axacndlem5  9755  axacnd  9756  opabdm  29966  opabrn  29967  pm14.122b  39462  pm14.123b  39465
  Copyright terms: Public domain W3C validator