Theorem frege55b 40598

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

Note that eqtr2 2819 incorporates eqcom 2805 which is stronger than this proposition which is identical to equcomi 2024. 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 40597	. 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2		dfsb1 2499	. . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)))
3		eqtr2 2819	. . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
4	3	exlimiv 1931	. . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
5	4	adantl 485	. . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥)
6	2, 5	sylbi 220	. 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥)
7	1, 6	syl 17	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781  [wsb 2069

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-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-13 2379  ax-ext 2770  ax-frege8 40510  ax-frege52c 40589

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721

This theorem is referenced by:  frege56b  40599