Metamath Proof Explorer


Theorem nfequid

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. (Contributed by NM, 13-Jan-2011) (Revised by NM, 21-Aug-2017)

Ref Expression
Assertion nfequid
|- F/ y x = x

Proof

Step Hyp Ref Expression
1 equid
 |-  x = x
2 1 nfth
 |-  F/ y x = x