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 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 2213

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

This theorem is used by:  nfbidf  2260  drex2  2471  rexbida  3274  opabbid  5170  zfrepclf  5246  dfid3  5553  oprabbid  7481  axrepndlem1  10626  axrepndlem2  10627  axrepnd  10628  axpowndlem2  10632  axpowndlem3  10633  axpowndlem4  10634  axregnd  10638  axinfndlem1  10639  axinfnd  10640  axacndlem4  10644  axacndlem5  10645  axacnd  10646  opabdm  33116  opabrn  33117  axtcond  37164  pm14.122b  45312  pm14.123b  45315  modelaxreplem3  45868  alsbid  50796