Theorem axc16ALT

Description: Alternate proof of axc16 , shorter but requiring ax-10 , ax-11 , ax-13 and using df-nf and df-sb . (Contributed by NM, 17-May-2008) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
2		ax-5	$$⊢\phi \to \forall z\phi$$
3	2	hbsb3	$$⊢\left[z/x\right]\phi \to \forall x\left[z/x\right]\phi$$
4	1 3	axc16i	$$⊢\forall xx=y\to \left(\phi \to \forall x\phi \right)$$