Theorem exbid 2129

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

Syntax hints:   → wi 4   ↔ wb 196  ∃wex 1744  Ⅎwnf 1748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750

This theorem is referenced by:  nfbidf  2130  mobid  2517  rexbida  3076  rexeqf  3165  opabbid  4748  zfrepclf  4810  dfid3  5054  oprabbid  6750  axrepndlem1  9452  axrepndlem2  9453  axrepnd  9454  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axregnd  9464  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  opabdm  29549  opabrn  29550  pm14.122b  38941  pm14.123b  38944