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

Note that eqtr2 2845 incorporates eqcom 2831 which is stronger than this proposition which is identical to equcomi 2025. 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 40514 . 2 (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2 dfsb1 2512 . . 3 ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)))
3 eqtr2 2845 . . . . 5 ((𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
43exlimiv 1932 . . . 4 (∃𝑧(𝑧 = 𝑦𝑧 = 𝑥) → 𝑦 = 𝑥)
54adantl 485 . . 3 (((𝑧 = 𝑦𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦𝑧 = 𝑥)) → 𝑦 = 𝑥)
62, 5sylbi 220 . 2 ([𝑦 / 𝑧]𝑧 = 𝑥𝑦 = 𝑥)
71, 6syl 17 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wex 1781  [wsb 2070
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-13 2392  ax-ext 2796  ax-frege8 40427  ax-frege52c 40506
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-sbc 3759
This theorem is referenced by:  frege56b  40516
  Copyright terms: Public domain W3C validator