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-41631,
ax-71790, ax-c92221, and ax-gen1618. This shows that this can be proved
without ax62003, even though the theorem equid1791 cannot be. A shorter
proof using ax62003 is obtainable from equid1791 and hbth1624.) Remark added
2-Dec-2015 NM: This proof does implicitly use ax6v1748,
which is used for
the derivation of axc92046, unless we consider ax-c92221 the starting axiom
rather than ax-131999. (Contributed by NM, 13-Jan-2011.) (Revised
by
Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)