Theorem exbid 2211

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1773  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfbidf  2212  drex2  2435  rexbida  3259  rexeqfOLD  3338  opabbid  5214  zfrepclf  5295  dfid3  5579  oprabbid  7485  axrepndlem1  10622  axrepndlem2  10623  axrepnd  10624  axpowndlem2  10628  axpowndlem3  10629  axpowndlem4  10630  axregnd  10634  axinfndlem1  10635  axinfnd  10636  axacndlem4  10640  axacndlem5  10641  axacnd  10642  opabdm  32500  opabrn  32501  pm14.122b  44007  pm14.123b  44010