Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hbequid | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 33189.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hbequid | ⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-c9 33193 | . 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥))) | |
2 | ax7 1930 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥)) | |
3 | 2 | pm2.43i 50 | . . . 4 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥) |
4 | 3 | alimi 1730 | . . 3 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑥) |
5 | 4 | a1d 25 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)) |
6 | 1, 5, 5 | pm2.61ii 176 | 1 ⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-c9 33193 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: nfequid-o 33213 equidq 33227 |
Copyright terms: Public domain | W3C validator |