Theorem equsexALT 2450

Description: Alternate proof of equsex 2449. This proves the result directly, instead of as a corollary of equsal 2448 via equs4 2447. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2403 is ax6e 2414. This proof mimics that of equsal 2448 (in particular, note that pm5.32i 585, exbii 1881, 19.41 2273, mpbiran 722 correspond respectively to pm5.74i 274, albii 1852, 19.23 2249, a1bi 365). (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 585	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓))
3	2	exbii 1881	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
4		ax6e 2414	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
5		equsal.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	19.41 2273	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓))
7	4, 6	mpbiran 722	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓)
8	3, 7	bitri 278	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃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 2215  ax-13 2403

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

This theorem is used by: (None)