Theorem hbequid 1152

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 1102, even though the theorem equid 1113 cannot be. A shorter proof that uses ax-9 1102 is obtainable from equid 1113 and hbth 977.)

Assertion

Ref	Expression
hbequid	|- (x = x -> A.x x = x)

Proof of Theorem hbequid

Step	Hyp	Ref	Expression
1		ax-12 1104	. . . 4 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
2	1	pm2.43i 64	. . 3 |- (-. A.x x = x -> (x = x -> A.x x = x))
3	2	com12 11	. 2 |- (x = x -> (-. A.x x = x -> A.x x = x))
4		pm2.18 81	. 2 |- ((-. A.x x = x -> A.x x = x) -> A.x x = x)
5	3, 4	syl 10	1 |- (x = x -> A.x x = x)

Syntax hints:  -. wn 2   -> wi 3  A.wal 950   = wceq 1099

This theorem is referenced by:  eubii 1364  mobii 1382

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

Copyright terms: Public domain