![]() |
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 39034. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2848 incorporates eqcom 2833 which is stronger than this proposition which is identical to equcomi 2123. 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 39031 | . 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | |
2 | df-sb 2070 | . . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥))) | |
3 | eqtr2 2848 | . . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥) | |
4 | 3 | exlimiv 2031 | . . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥) |
5 | 4 | adantl 475 | . . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥) |
6 | 2, 5 | sylbi 209 | . 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∃wex 1880 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-12 2222 ax-13 2391 ax-ext 2804 ax-frege8 38944 ax-frege52c 39023 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-sbc 3664 |
This theorem is referenced by: frege56b 39033 |
Copyright terms: Public domain | W3C validator |