Theorem exbid 2228

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

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

This theorem is referenced by:  nfbidf  2229  drex2  2444  rexbida  3246  rexeqfOLD  3325  opabbid  5161  zfrepclf  5234  dfid3  5520  oprabbid  7421  axrepndlem1  10501  axrepndlem2  10502  axrepnd  10503  axpowndlem2  10507  axpowndlem3  10508  axpowndlem4  10509  axregnd  10513  axinfndlem1  10514  axinfnd  10515  axacndlem4  10519  axacndlem5  10520  axacnd  10521  opabdm  32638  opabrn  32639  pm14.122b  44606  pm14.123b  44609  modelaxreplem3  45163