Theorem nfequid-o

Description: Bound-variable hypothesis builder for x = x . This theorem tells us that any variable, including x , is effectively not free in x = x , even though x is technically free according to the traditional definition of free variable. (The proof uses only ax-4 , ax-7 , ax-c9 , and ax-gen . This shows that this can be proved without ax6 , even though Theorem equid cannot. A shorter proof using ax6 is obtainable from equid and hbth .) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v , which is used for the derivation of axc9 , unless we consider ax-c9 the starting axiom rather than ax-13 . (Contributed by NM, 13-Jan-2011) (Revised by Mario Carneiro, 12-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nfequid-o	$$⊢Ⅎyx=x$$

Proof

Step	Hyp	Ref	Expression
1		hbequid	$$⊢x=x\to \forall yx=x$$
2	1	nf5i	$$⊢Ⅎyx=x$$