Theorem exbid 2222

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1778  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783

This theorem is referenced by:  nfbidf  2223  drex2  2446  rexbida  3271  rexeqfOLD  3354  opabbid  5207  zfrepclf  5290  dfid3  5580  oprabbid  7499  axrepndlem1  10633  axrepndlem2  10634  axrepnd  10635  axpowndlem2  10639  axpowndlem3  10640  axpowndlem4  10641  axregnd  10645  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  opabdm  32624  opabrn  32625  pm14.122b  44447  pm14.123b  44450  modelaxreplem3  45002