Theorem equsexALT 2427

Description: Alternate proof of equsex 2426. This proves the result directly, instead of as a corollary of equsal 2425 via equs4 2424. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2380 is ax6e 2391. This proof mimics that of equsal 2425 (in particular, note that pm5.32i 574, exbii 1846, 19.41 2236, mpbiran 708 correspond respectively to pm5.74i 271, albii 1817, 19.23 2212, a1bi 362). (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 574	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓))
3	2	exbii 1846	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
4		ax6e 2391	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
5		equsal.1	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	19.41 2236	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓))
7	4, 6	mpbiran 708	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓)
8	3, 7	bitri 275	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1777  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178  ax-13 2380

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782

This theorem is referenced by: (None)