Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax7 | Structured version Visualization version GIF version |
Description: Proof of ax-7 2016
from ax7v1 2018 and ax7v2 2019 (and earlier axioms), proving
sufficiency of the conjunction of the latter two weakened versions of
ax7v 2017, which is itself a weakened version of ax-7 2016.
Note that the weakened version of ax-7 2016 obtained by adding a disjoint variable condition on 𝑥, 𝑧 (resp. on 𝑦, 𝑧) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.) |
Ref | Expression |
---|---|
ax7 | ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax7v2 2019 | . . . 4 ⊢ (𝑥 = 𝑡 → (𝑥 = 𝑦 → 𝑡 = 𝑦)) | |
2 | ax7v2 2019 | . . . 4 ⊢ (𝑥 = 𝑡 → (𝑥 = 𝑧 → 𝑡 = 𝑧)) | |
3 | ax7v1 2018 | . . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 = 𝑧 → 𝑦 = 𝑧)) | |
4 | 3 | imp 410 | . . . . 5 ⊢ ((𝑡 = 𝑦 ∧ 𝑡 = 𝑧) → 𝑦 = 𝑧) |
5 | 4 | a1i 11 | . . . 4 ⊢ (𝑥 = 𝑡 → ((𝑡 = 𝑦 ∧ 𝑡 = 𝑧) → 𝑦 = 𝑧)) |
6 | 1, 2, 5 | syl2and 611 | . . 3 ⊢ (𝑥 = 𝑡 → ((𝑥 = 𝑦 ∧ 𝑥 = 𝑧) → 𝑦 = 𝑧)) |
7 | ax6evr 2023 | . . 3 ⊢ ∃𝑡 𝑥 = 𝑡 | |
8 | 6, 7 | exlimiiv 1939 | . 2 ⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑧) → 𝑦 = 𝑧) |
9 | 8 | ex 416 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 |
This theorem is referenced by: equcomi 2025 equtr 2029 equequ1 2033 cbvaev 2059 aeveq 2062 axc16i 2435 equvel 2455 mo4 2565 axextnd 10202 bj-dtru 34733 wl-aetr 35422 wl-exeq 35427 wl-aleq 35428 wl-nfeqfb 35429 equcomi1 36649 hbequid 36658 equidqe 36671 aev-o 36680 ax6e2eq 41848 ax6e2eqVD 42198 2reu8i 44275 |
Copyright terms: Public domain | W3C validator |