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 43564
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.)

Assertion
Ref Expression
frege55b (𝑥 = 𝑦𝑦 = 𝑥)

Proof of Theorem frege55b
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 frege55lem2b 43563 . 2 (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2 dfsb1 2475 . . 3 ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)))
3 eqtr2 2750 . . . . 5 ((𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
43exlimiv 1926 . . . 4 (∃𝑧(𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
54adantl 480 . . 3 (((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)) → 𝑦 = 𝑥)
62, 5sylbi 216 . 2 ([𝑦 / 𝑧]𝑧 = 𝑥𝑦 = 𝑥)
71, 6syl 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