This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ Ⅎ 𝑦 𝑥 = 𝑥

Proof

Step	Hyp	Ref	Expression
1		equid	⊢ 𝑥 = 𝑥
2	1	nfth	⊢ Ⅎ 𝑦 𝑥 = 𝑥