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 1899	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfbidf  2260  drex2  2471  rexbida  3274  opabbid  5169  zfrepclf  5243  dfid3  5548  oprabbid  7485  axrepndlem1  10677  axrepndlem2  10678  axrepnd  10679  axpowndlem2  10683  axpowndlem3  10684  axpowndlem4  10685  axregnd  10689  axinfndlem1  10690  axinfnd  10691  axacndlem4  10695  axacndlem5  10696  axacnd  10697  opabdm  33205  opabrn  33206  axtcond  37266  pm14.122b  45407  pm14.123b  45410  modelaxreplem3  45970  alsbid  50898