Theorem hbequid 1167

Description: Bound-variable hypothesis builder for x = x. This theorem tells us that x is effectively not free in x = x, even though it is technically free according to the traditional definition of free variable. (The proof shows that this can be proved without ax-9 963, even though the theorem equid 1124 cannot be. A shorter proof that uses ax-9 963 is obtainable from equid 1124 and hbth 999.)

Assertion

Ref	Expression
hbequid	⊢ (x = x → ∀x x = x)

Proof of Theorem hbequid

Step	Hyp	Ref	Expression
1		ax-12 966	. . . 4 ⊢ (¬ ∀x x = x → (¬ ∀x x = x → (x = x → ∀x x = x)))
2	1	pm2.43i 64	. . 3 ⊢ (¬ ∀x x = x → (x = x → ∀x x = x))
3	2	com12 11	. 2 ⊢ (x = x → (¬ ∀x x = x → ∀x x = x))
4		pm2.18 81	. 2 ⊢ ((¬ ∀x x = x → ∀x x = x) → ∀x x = x)
5	3, 4	syl 10	1 ⊢ (x = x → ∀x x = x)

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 952   = wceq 954

This theorem is referenced by:  eubii 1385  mobii 1403

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-12 966

Copyright terms: Public domain