Theorem hbequid 1169

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

Assertion

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

Proof of Theorem hbequid

Step	Hyp	Ref	Expression
1		ax-12 968	. 2 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
2		ax-1 4	. 2 |- (A.x x = x -> (x = x -> A.x x = x))
3	1, 2, 2	pm2.61ii 130	1 |- (x = x -> A.x x = x)

Syntax hints:   -> wi 3  A.wal 954   = wceq 956

This theorem is referenced by:  eubii 1387  mobii 1405

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

Copyright terms: Public domain