![]() |
Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > frege55b | Structured version Visualization version GIF version |
Description: Lemma for frege57b 43566. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2750 incorporates eqcom 2733 which is stronger than this proposition which is identical to equcomi 2013. 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.) |
Ref | Expression |
---|---|
frege55b | ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege55lem2b 43563 | . 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | |
2 | dfsb1 2475 | . . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥))) | |
3 | eqtr2 2750 | . . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥) | |
4 | 3 | exlimiv 1926 | . . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥) |
5 | 4 | adantl 480 | . . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥) |
6 | 2, 5 | sylbi 216 | . 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∃wex 1774 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-12 2167 ax-13 2366 ax-ext 2697 ax-frege8 43476 ax-frege52c 43555 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-sbc 3777 |
This theorem is referenced by: frege56b 43565 |
Copyright terms: Public domain | W3C validator |