Theorem ax12vALT

Description: Alternate proof of ax12v2 , shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1	$$⊢\phi \to \left(x=y\to \phi \right)$$
2		axc16	$$⊢\forall xx=y\to \left(\left(x=y\to \phi \right)\to \forall x\left(x=y\to \phi \right)\right)$$
3	1 2	syl5	$$⊢\forall xx=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
4	3	a1d	$$⊢\forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
5		axc15	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
6	4 5	pm2.61i	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$