Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frege55b Structured version   Visualization version   GIF version

Theorem frege55b 42257
Description: Lemma for frege57b 42259. Proposition 55 of [Frege1879] p. 50.

Note that eqtr2 2757 incorporates eqcom 2740 which is stronger than this proposition which is identical to equcomi 2021. 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.
StepHypRef Expression
1 frege55lem2b 42256 . 2 (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2 dfsb1 2480 . . 3 ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)))
3 eqtr2 2757 . . . . 5 ((𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
43exlimiv 1934 . . . 4 (∃𝑧(𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
54adantl 483 . . 3 (((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)) → 𝑦 = 𝑥)
62, 5sylbi 216 . 2 ([𝑦 / 𝑧]𝑧 = 𝑥𝑦 = 𝑥)
71, 6syl 17 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1782  [wsb 2068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-13 2371  ax-ext 2704  ax-frege8 42169  ax-frege52c 42248
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3741
This theorem is referenced by:  frege56b  42258
  Copyright terms: Public domain W3C validator