Metamath Proof Explorer


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
|- F/ y x = x

Proof

Step Hyp Ref Expression
1 hbequid
 |-  ( x = x -> A. y x = x )
2 1 nf5i
 |-  F/ y x = x