Theorem frege55b 44350

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

Note that eqtr2 2760 incorporates eqcom 2746 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 44349	. 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2		dfsb1 2489	. . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)))
3		eqtr2 2760	. . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
4	3	exlimiv 1937	. . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
5	4	adantl 482	. . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥)
6	2, 5	sylbi 218	. 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥)
7	1, 6	syl 17	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-13 2380  ax-ext 2711  ax-frege8 44262  ax-frege52c 44341

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-sbc 3724

This theorem is referenced by:  frege56b  44351