Theorem equsexALT 2282

Description: Alternate proof of equsex 2281. This proves the result directly, instead of as a corollary of equsal 2279 via equs4 2278. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2234 is ax6e 2238. This proof mimics that of equsal 2279 (in particular, note pm5.32i 667, exbii 1764, 19.41 2090, mpbiran 955 correspond respectively to pm5.74i 259, albii 1737, 19.23 2067, a1bi 351). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
equsex.nf	⊢ Ⅎ𝑥𝜓
equsex.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

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

Proof of Theorem equsexALT

Step	Hyp	Ref	Expression
1		equsex.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	pm5.32i 667	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜓))
3	2	exbii 1764	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
4		ax6e 2238	. . 3 ⊢ ∃𝑥 𝑥 = 𝑦
5		equsex.nf	. . . 4 ⊢ Ⅎ𝑥𝜓
6	5	19.41 2090	. . 3 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ (∃𝑥 𝑥 = 𝑦 ∧ 𝜓))
7	4, 6	mpbiran 955	. 2 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜓)
8	3, 7	bitri 263	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∃wex 1695  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701

This theorem is referenced by: (None)