Theorem equsexALT 2419

Description: Alternate proof of equsex 2418. This proves the result directly, instead of as a corollary of equsal 2417 via equs4 2416. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2372 is ax6e 2383. This proof mimics that of equsal 2417 (in particular, note that pm5.32i 575, exbii 1850, 19.41 2228, mpbiran 706 correspond respectively to pm5.74i 270, albii 1822, 19.23 2204, a1bi 363). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
equsal.1	⊢ Ⅎ𝑥𝜓
equsal.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
equsexALT	⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Proof of Theorem equsexALT

Step	Hyp	Ref	Expression
1		equsal.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	pm5.32i 575	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓))
3	2	exbii 1850	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
4		ax6e 2383	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
5		equsal.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	19.41 2228	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓))
7	4, 6	mpbiran 706	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓)
8	3, 7	bitri 274	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171  ax-13 2372

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787

This theorem is referenced by: (None)