Theorem equs5e

A property related to substitution that unlike equs5 does not require a distinctor antecedent. This proof uses ax12, see equs5eALT for an alternative one using [ax-12] but not ax13. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.)

Conclusion
\( \vdash \exists x \, (x = y \wedge \varphi) \rightarrow \forall x \, (x = y \rightarrow \exists y \, \varphi) \)
Proof
l0
nfa1
l1
ax12
\( \vdash x = y \rightarrow \forall y \, \exists y \, \varphi \rightarrow \forall x \, (x = y \rightarrow \exists y \, \varphi) \)
hbe1
\( \vdash \exists y \, \varphi \rightarrow \forall y \, \exists y \, \varphi \)
19.23bi _
\( \vdash \varphi \rightarrow \forall y \, \exists y \, \varphi \)
impel l1 _
exlimi l0 _