Theorem exbid 2221

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

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1776  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfbidf  2222  drex2  2445  rexbida  3270  rexeqfOLD  3353  opabbid  5213  zfrepclf  5297  dfid3  5586  oprabbid  7498  axrepndlem1  10630  axrepndlem2  10631  axrepnd  10632  axpowndlem2  10636  axpowndlem3  10637  axpowndlem4  10638  axregnd  10642  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  opabdm  32631  opabrn  32632  pm14.122b  44419  pm14.123b  44422  modelaxreplem3  44945