Metamath Proof Explorer

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 ¬ x = y y = z x y = z


Step Hyp Ref Expression
1 ax-13 ¬ x = y y = z x y = z