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