Theorem frege55b 42291

Description: Lemma for frege57b 42293. Proposition 55 of [Frege1879] p. 50.

Note that eqtr2 2755 incorporates eqcom 2738 which is stronger than this proposition which is identical to equcomi 2020. Is it possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
frege55b	⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Proof of Theorem frege55b

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		frege55lem2b 42290	. 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2		dfsb1 2479	. . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)))
3		eqtr2 2755	. . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
4	3	exlimiv 1933	. . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
5	4	adantl 482	. . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥)
6	2, 5	sylbi 216	. 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥)
7	1, 6	syl 17	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781  [wsb 2067

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-13 2370  ax-ext 2702  ax-frege8 42203  ax-frege52c 42282

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-sbc 3743

This theorem is referenced by:  frege56b  42292