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

Theorem exbid 2215
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 2185 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3exbidh 1859 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wex 1771  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-nf 1776
This theorem is referenced by:  nfbidf  2216  drex2  2456  rexbida  3315  rexeqf  3396  opabbid  5122  zfrepclf  5189  dfid3  5455  oprabbid  7208  axrepndlem1  10002  axrepndlem2  10003  axrepnd  10004  axpowndlem2  10008  axpowndlem3  10009  axpowndlem4  10010  axregnd  10014  axinfndlem1  10015  axinfnd  10016  axacndlem4  10020  axacndlem5  10021  axacnd  10022  opabdm  30290  opabrn  30291  pm14.122b  40632  pm14.123b  40635
  Copyright terms: Public domain W3C validator