Theorem ax13w

Description: Weak version (principal instance) of ax-13 . (Because y and z don't need to be distinct, this actually bundles the principal instance and the degenerate instance ( -. x = y -> ( y = y -> A. x y = y ) ) .) Uses only Tarski's FOL axiom schemes. The proof is trivial but is included to complete the set ax10w , ax11w , and ax12w . (Contributed by NM, 10-Apr-2017)

	Ref	Expression
Assertion	ax13w	$$⊢\neg x=y\to \left(y=z\to \forall xy=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax5d	$$⊢\neg x=y\to \left(y=z\to \forall xy=z\right)$$