Theorem exbid 2258

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

Step	Hyp	Ref	Expression
1		albid.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nf5ri 2229	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	exbidh 1955	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 197  ∃wex 1859  Ⅎwnf 1863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-12 2213

This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864

This theorem is referenced by:  nfbidf  2259  drex2  2489  mobid  2648  rexbida  3231  rexeqf  3320  opabbid  4902  zfrepclf  4964  dfid3  5214  oprabbid  6932  axrepndlem1  9693  axrepndlem2  9694  axrepnd  9695  axpowndlem2  9699  axpowndlem3  9700  axpowndlem4  9701  axregnd  9705  axinfndlem1  9706  axinfnd  9707  axacndlem4  9711  axacndlem5  9712  axacnd  9713  opabdm  29742  opabrn  29743  pm14.122b  39117  pm14.123b  39120