Theorem equs45f

Two ways of expressing substitution when \( y \) is not free in \( \varphi \). The implication "to the left" is equs4 and does not require the nonfreeness hypothesis. Theorem sbalex replaces the nonfreeness hypothesis with a disjoint variable condition and equs5 replaces it with a distinctor antecedent. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on [ax-13]. Use sbalex instead. (New usage is discouraged.)

Hypothesis
equs45f.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists x \, (x = y \wedge \varphi) \leftrightarrow \forall x \, (x = y \rightarrow \varphi) \)
Proof
equs45f.1
nf5ri _
anim2i _
l3
eximi _
\( \vdash \exists x \, (x = y \wedge \varphi) \rightarrow \exists x \, (x = y \wedge \forall y \, \varphi) \)
equs5a
\( \vdash \exists x \, (x = y \wedge \forall y \, \varphi) \rightarrow \forall x \, (x = y \rightarrow \varphi) \)
l5
syl l3 _
equs4
impbii l5 _