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

Theorem exbid 2222
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 2194 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1866 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wex 1778  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783
This theorem is referenced by:  nfbidf  2223  drex2  2446  rexbida  3271  rexeqfOLD  3354  opabbid  5207  zfrepclf  5290  dfid3  5580  oprabbid  7499  axrepndlem1  10633  axrepndlem2  10634  axrepnd  10635  axpowndlem2  10639  axpowndlem3  10640  axpowndlem4  10641  axregnd  10645  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  opabdm  32624  opabrn  32625  pm14.122b  44447  pm14.123b  44450  modelaxreplem3  45002
  Copyright terms: Public domain W3C validator