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 42730
Description: Lemma for frege57b 42732. Proposition 55 of [Frege1879] p. 50.

Note that eqtr2 2756 incorporates eqcom 2739 which is stronger than this proposition which is identical to equcomi 2020. 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 42729 . 2 (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2 dfsb1 2480 . . 3 ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)))
3 eqtr2 2756 . . . . 5 ((𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
43exlimiv 1933 . . . 4 (∃𝑧(𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
54adantl 482 . . 3 (((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)) → 𝑦 = 𝑥)
62, 5sylbi 216 . 2 ([𝑦 / 𝑧]𝑧 = 𝑥𝑦 = 𝑥)
71, 6syl 17 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1781  [wsb 2067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-13 2371  ax-ext 2703  ax-frege8 42642  ax-frege52c 42721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778
This theorem is referenced by:  frege56b  42731
  Copyright terms: Public domain W3C validator