Theorem exbid 2220

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 2192	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	exbidh 1874	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1786  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 206  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfbidf  2221  drex2  2444  rexbida  3249  rexeqf  3332  opabbid  5144  zfrepclf  5222  dfid3  5492  oprabbid  7332  axrepndlem1  10347  axrepndlem2  10348  axrepnd  10349  axpowndlem2  10353  axpowndlem3  10354  axpowndlem4  10355  axregnd  10359  axinfndlem1  10360  axinfnd  10361  axacndlem4  10365  axacndlem5  10366  axacnd  10367  opabdm  30945  opabrn  30946  pm14.122b  42009  pm14.123b  42012