Theorem equsexALT 2430

Description: Alternate proof of equsex 2429. This proves the result directly, instead of as a corollary of equsal 2428 via equs4 2427. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2379 is ax6e 2390. This proof mimics that of equsal 2428 (in particular, note that pm5.32i 578, exbii 1849, 19.41 2235, mpbiran 708 correspond respectively to pm5.74i 274, albii 1821, 19.23 2209, a1bi 366). (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 578	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓))
3	2	exbii 1849	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
4		ax6e 2390	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
5		equsal.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	19.41 2235	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓))
7	4, 6	mpbiran 708	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓)
8	3, 7	bitri 278	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175  ax-13 2379

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786

This theorem is referenced by: (None)