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)