![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > equid1 | Structured version Visualization version GIF version |
Description: Proof of equid 2118 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 2011; see the proof of equid 2118. See equid1ALT 35000 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
equid1 | ⊢ 𝑥 = 𝑥 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-c4 34959 | . . . 4 ⊢ (∀𝑥(∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) → (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))) | |
2 | ax-c5 34958 | . . . . 5 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ¬ ∀𝑥 𝑥 = 𝑥) | |
3 | ax-c9 34965 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑥 → (¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))) | |
4 | 2, 2, 3 | sylc 65 | . . . 4 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) |
5 | 1, 4 | mpg 1898 | . . 3 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) |
6 | ax-c10 34961 | . . 3 ⊢ (∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) → 𝑥 = 𝑥) | |
7 | 5, 6 | syl 17 | . 2 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥) |
8 | ax-c7 34960 | . 2 ⊢ (¬ ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥) | |
9 | 7, 8 | pm2.61i 177 | 1 ⊢ 𝑥 = 𝑥 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1656 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-c5 34958 ax-c4 34959 ax-c7 34960 ax-c10 34961 ax-c9 34965 |
This theorem is referenced by: equcomi1 34975 |
Copyright terms: Public domain | W3C validator |