Theorem exbid 2259

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1809  Ⅎwnf 1813

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is used by:  nfbidf  2260  drex2  2474  rexbida  3277  opabbid  5176  zfrepclf  5252  dfid3  5559  oprabbid  7475  axrepndlem1  10581  axrepndlem2  10582  axrepnd  10583  axpowndlem2  10587  axpowndlem3  10588  axpowndlem4  10589  axregnd  10593  axinfndlem1  10594  axinfnd  10595  axacndlem4  10599  axacndlem5  10600  axacnd  10601  opabdm  32965  opabrn  32966  axtcond  37017  pm14.122b  45161  pm14.123b  45164  modelaxreplem3  45717  alsbid  50608