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

Theorem exbid 2221
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 2191 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1864 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wex 1776  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173
This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781
This theorem is referenced by:  nfbidf  2222  drex2  2460  rexbida  3318  rexeqf  3398  opabbid  5123  zfrepclf  5190  dfid3  5456  oprabbid  7213  axrepndlem1  10008  axrepndlem2  10009  axrepnd  10010  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axregnd  10020  axinfndlem1  10021  axinfnd  10022  axacndlem4  10026  axacndlem5  10027  axacnd  10028  opabdm  30356  opabrn  30357  pm14.122b  40748  pm14.123b  40751
  Copyright terms: Public domain W3C validator