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 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-13 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) |