Theorem axc15

Derivation of set.mm's original [ax-c15] from [ax-c11n] and the shorter [ax-12] that has replaced it.

Theorem ax12 shows the reverse derivation of [ax-12] from [ax-c15].

Normally, axc15 should be used rather than [ax-c15], except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
Proof
l0
ax6ev
\( \vdash \exists z \, z = y' \)
l1
dveeq2
\( \vdash \neg \forall x \, x = y' \rightarrow z = y' \rightarrow \forall x \, z = y' \)
l2
ax12v
\( \vdash x = z \rightarrow \varphi \rightarrow \forall x \, (x = z \rightarrow \varphi) \)
l3
equeuclr
l4
sps _
imim1d l3
al2imi _
imim2d _
imim12d l4 _
\( \vdash \forall x \, z = y' \rightarrow (x = z \rightarrow \varphi \rightarrow \forall x \, (x = z \rightarrow \varphi)) \rightarrow x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
syl6mpi l1 l2 _
exlimdv _
\( \vdash \neg \forall x \, x = y' \rightarrow \exists z \, z = y' \rightarrow x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
mpi l0 _