Theorem hbequid 1165

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

Assertion

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

Proof of Theorem hbequid

Step	Hyp	Ref	Expression
1		ax-12 965	. . . 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 951   = wceq 953

This theorem is referenced by:  eubii 1380  mobii 1398

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

Copyright terms: Public domain