Theorem axc15

Description: 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.)

	Ref	Expression
Assertion	axc15	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$$⊢\exists zz=y$$
2		dveeq2	$$⊢\neg \forall xx=y\to \left(z=y\to \forall xz=y\right)$$
3		ax12v	$$⊢x=z\to \left(\phi \to \forall x\left(x=z\to \phi \right)\right)$$
4		equeuclr	$$⊢z=y\to \left(x=y\to x=z\right)$$
5	4	sps	$$⊢\forall xz=y\to \left(x=y\to x=z\right)$$
6	4	imim1d	$$⊢z=y\to \left(\left(x=z\to \phi \right)\to \left(x=y\to \phi \right)\right)$$
7	6	al2imi	$$⊢\forall xz=y\to \left(\forall x\left(x=z\to \phi \right)\to \forall x\left(x=y\to \phi \right)\right)$$
8	7	imim2d	$$⊢\forall xz=y\to \left(\left(\phi \to \forall x\left(x=z\to \phi \right)\right)\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
9	5 8	imim12d	$$⊢\forall xz=y\to \left(\left(x=z\to \left(\phi \to \forall x\left(x=z\to \phi \right)\right)\right)\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)\right)$$
10	2 3 9	syl6mpi	$$⊢\neg \forall xx=y\to \left(z=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)\right)$$
11	10	exlimdv	$$⊢\neg \forall xx=y\to \left(\exists zz=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)\right)$$
12	1 11	mpi	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$