Theorem ax13v

Description: A weaker version of ax-13 with distinct variable restrictions on pairs x , z and y , z . In order to show (with ax13 ) that this weakening is still adequate, this should be the only theorem referencing ax-13 directly.

Had we additionally required x and y be distinct, too, this theorem would have been a direct consequence of ax-5 . So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. Preferably, use the version ax13w to avoid the propagation of ax-13 . (Contributed by NM, 30-Jun-2016) (New usage is discouraged.)

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

Proof

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