Theorem exbid 2226

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 2198	. 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 2180

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

This theorem is referenced by:  nfbidf  2227  drex2  2442  rexbida  3244  rexeqfOLD  3323  opabbid  5154  zfrepclf  5227  dfid3  5512  oprabbid  7411  axrepndlem1  10483  axrepndlem2  10484  axrepnd  10485  axpowndlem2  10489  axpowndlem3  10490  axpowndlem4  10491  axregnd  10495  axinfndlem1  10496  axinfnd  10497  axacndlem4  10501  axacndlem5  10502  axacnd  10503  opabdm  32594  opabrn  32595  pm14.122b  44515  pm14.123b  44518  modelaxreplem3  45072