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

Theorem exbid 2089
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 2063 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1791 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfbidf  2090  mobid  2488  rexbida  3040  rexeqf  3124  opabbid  4677  zfrepclf  4737  dfid3  4990  oprabbid  6661  axrepndlem1  9358  axrepndlem2  9359  axrepnd  9360  axpowndlem2  9364  axpowndlem3  9365  axpowndlem4  9366  axregnd  9370  axinfndlem1  9371  axinfnd  9372  axacndlem4  9376  axacndlem5  9377  axacnd  9378  opabdm  29266  opabrn  29267  pm14.122b  38106  pm14.123b  38109
  Copyright terms: Public domain W3C validator