Theorem equs5av

A property related to substitution that replaces the distinctor from equs5 to a disjoint variable condition. Version of equs5a with a disjoint variable condition, which does not require [ax-13]. See also sbalex. (Contributed by NM, 2-Feb-2007.) (Revised by GG, 15-Dec-2023.)

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