Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  equid1 Unicode version

Theorem equid1 2237
 Description: Proof of equid 1791 from our older axioms. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and requires no dummy variables. A simpler proof, similar to Tarski's, is possible if we make use of ax-5 1704; see the proof of equid 1791. See equid1ALT 2255 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
equid1

Proof of Theorem equid1
StepHypRef Expression
1 ax-c4 2215 . . . 4
2 ax-c5 2214 . . . . 5
3 ax-c9 2221 . . . . 5
42, 2, 3sylc 60 . . . 4
51, 4mpg 1620 . . 3
6 ax-c10 2217 . . 3
75, 6syl 16 . 2
8 ax-c7 2216 . 2
97, 8pm2.61i 164 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  A.wal 1393 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-c5 2214  ax-c4 2215  ax-c7 2216  ax-c10 2217  ax-c9 2221
 Copyright terms: Public domain W3C validator