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

Note that eqtr2 2629 incorporates eqcom 2616 which is stronger than this proposition which is identical to equcomi 1930. Is is 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 37013 . 2 (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2 df-sb 1867 . . 3 ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)))
3 eqtr2 2629 . . . . 5 ((𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
43exlimiv 1844 . . . 4 (∃𝑧(𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
54adantl 480 . . 3 (((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)) → 𝑦 = 𝑥)
62, 5sylbi 205 . 2 ([𝑦 / 𝑧]𝑧 = 𝑥𝑦 = 𝑥)
71, 6syl 17 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1694  [wsb 1866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2032  ax-13 2232  ax-ext 2589  ax-frege8 36926  ax-frege52c 37005
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-sbc 3402
This theorem is referenced by:  frege56b  37015
  Copyright terms: Public domain W3C validator