Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  equid1 Structured version   Visualization version   GIF version

Theorem equid1 36188
Description: Proof of equid 2019 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 1911; see the proof of equid 2019. See equid1ALT 36214 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 36173 . . . 4 (∀𝑥(∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) → (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)))
2 ax-c5 36172 . . . . 5 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ¬ ∀𝑥 𝑥 = 𝑥)
3 ax-c9 36179 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑥 → (¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)))
42, 2, 3sylc 65 . . . 4 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
51, 4mpg 1799 . . 3 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
6 ax-c10 36175 . . 3 (∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) → 𝑥 = 𝑥)
75, 6syl 17 . 2 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥𝑥 = 𝑥)
8 ax-c7 36174 . 2 (¬ ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥𝑥 = 𝑥)
97, 8pm2.61i 185 1 𝑥 = 𝑥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-c5 36172  ax-c4 36173  ax-c7 36174  ax-c10 36175  ax-c9 36179
This theorem is referenced by:  equcomi1  36189
  Copyright terms: Public domain W3C validator