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	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ax5d	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )