This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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