Theorem exbid 2091

Description: Formula-building rule for existential quantifier (deduction rule). (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 2065	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	exbidh 1794	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∃wex 1704  Ⅎwnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfbidf  2092  mobid  2489  rexbida  3047  rexeqf  3135  opabbid  4715  zfrepclf  4777  dfid3  5025  oprabbid  6708  axrepndlem1  9414  axrepndlem2  9415  axrepnd  9416  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axregnd  9426  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  opabdm  29423  opabrn  29424  pm14.122b  38624  pm14.123b  38627