Theorem axc11r

Same as axc11 but with reversed antecedent. Note the use of [ax-12] (and not merely ax12v as in axc11rv ).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev and aecom, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with [ax-13] only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.)

Conclusion
\( \vdash \forall y \, y = x \rightarrow \forall x \, \varphi \rightarrow \forall y \, \varphi \)
Proof
ax-12
l1
sps _
\( \vdash \forall y \, y = x \rightarrow \forall x \, \varphi \rightarrow \forall y \, (y = x \rightarrow \varphi) \)
pm2.27
al2imi _
\( \vdash \forall y \, y = x \rightarrow \forall y \, (y = x \rightarrow \varphi) \rightarrow \forall y \, \varphi \)
syld l1 _