Theorem exbid 2263

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 2235	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  nfbidf  2264  drex2  2474  rexbida  3278  opabbid  5173  zfrepclf  5247  dfid3  5553  oprabbid  7505  axrepndlem1  10701  axrepndlem2  10702  axrepnd  10703  axpowndlem2  10707  axpowndlem3  10708  axpowndlem4  10709  axregnd  10713  axinfndlem1  10714  axinfnd  10715  axacndlem4  10719  axacndlem5  10720  axacnd  10721  opabdm  33274  opabrn  33275  axtcond  37443  pm14.122b  45596  pm14.123b  45599  modelaxreplem3  46163  alsbid  51176