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 40123. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2839 incorporates eqcom 2825 which is stronger than this proposition which is identical to equcomi 2015. 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 40120 | . 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | |
2 | dfsb1 2503 | . . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥))) | |
3 | eqtr2 2839 | . . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥) | |
4 | 3 | exlimiv 1922 | . . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥) |
5 | 4 | adantl 482 | . . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥) |
6 | 2, 5 | sylbi 218 | . 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥) |
7 | 1, 6 | syl 17 | 1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1771 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-12 2167 ax-13 2381 ax-ext 2790 ax-frege8 40033 ax-frege52c 40112 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-sbc 3770 |
This theorem is referenced by: frege56b 40122 |
Copyright terms: Public domain | W3C validator |