Theorem equs5a

A property related to substitution that unlike equs5 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on [ax-13]. This proof uses ax12, see equs5aALT for an alternative one using [ax-12] but not ax13. Usage of the weaker equs5av is preferred, which uses ax12v2, but not [ax-13]. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)

Conclusion
\( \vdash \exists x \, (x = y \wedge \forall y \, \varphi) \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
Proof
l0
nfa1
ax12
imp _
exlimi l0 _