Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > aeveq | Structured version Visualization version GIF version |
Description: The antecedent ∀𝑥𝑥 = 𝑦 with a disjoint variable condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.) |
Ref | Expression |
---|---|
aeveq | ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aevlem 2056 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑢 𝑢 = 𝑧) | |
2 | ax6ev 1971 | . . 3 ⊢ ∃𝑢 𝑢 = 𝑡 | |
3 | ax7 2017 | . . . 4 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑡 → 𝑧 = 𝑡)) | |
4 | 3 | aleximi 1832 | . . 3 ⊢ (∀𝑢 𝑢 = 𝑧 → (∃𝑢 𝑢 = 𝑡 → ∃𝑢 𝑧 = 𝑡)) |
5 | 2, 4 | mpi 20 | . 2 ⊢ (∀𝑢 𝑢 = 𝑧 → ∃𝑢 𝑧 = 𝑡) |
6 | ax5e 1913 | . 2 ⊢ (∃𝑢 𝑧 = 𝑡 → 𝑧 = 𝑡) | |
7 | 1, 5, 6 | 3syl 18 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 ∃wex 1779 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1780 |
This theorem is referenced by: aev 2058 2ax6e 2469 aevdemo 28865 wl-moteq 35714 wl-spae 35721 |
Copyright terms: Public domain | W3C validator |