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

Theorem exbid 2129
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 2103 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1834 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wex 1744  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfbidf  2130  mobid  2517  rexbida  3076  rexeqf  3165  opabbid  4748  zfrepclf  4810  dfid3  5054  oprabbid  6750  axrepndlem1  9452  axrepndlem2  9453  axrepnd  9454  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axregnd  9464  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  opabdm  29549  opabrn  29550  pm14.122b  38941  pm14.123b  38944
  Copyright terms: Public domain W3C validator