Theorem exbid 2261

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfbidf  2262  drex2  2473  rexbida  3276  opabbid  5174  zfrepclf  5250  dfid3  5557  oprabbid  7481  axrepndlem1  10602  axrepndlem2  10603  axrepnd  10604  axpowndlem2  10608  axpowndlem3  10609  axpowndlem4  10610  axregnd  10614  axinfndlem1  10615  axinfnd  10616  axacndlem4  10620  axacndlem5  10621  axacnd  10622  opabdm  33069  opabrn  33070  axtcond  37082  pm14.122b  45232  pm14.123b  45235  modelaxreplem3  45788  alsbid  50713