![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > axc11n | Structured version Visualization version GIF version |
Description: Derive set.mm's original ax-c11n 38869 from others. Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). If a disjoint variable condition is added on 𝑥 and 𝑦, then this becomes an instance of aevlem 2052. Use aecom 2429 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 2-Jul-2021.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axc11n | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dveeq1 2382 | . . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) | |
2 | 1 | com12 32 | . . . 4 ⊢ (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧)) |
3 | axc11r 2368 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)) | |
4 | aev 2054 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) | |
5 | 3, 4 | syl6 35 | . . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)) |
6 | 2, 5 | syl9 77 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))) |
7 | ax6evr 2011 | . . 3 ⊢ ∃𝑧 𝑥 = 𝑧 | |
8 | 6, 7 | exlimiiv 1928 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)) |
9 | 8 | pm2.18d 127 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-10 2138 ax-12 2174 ax-13 2374 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-nf 1780 |
This theorem is referenced by: aecom 2429 axi10 2702 wl-hbae1 37499 wl-ax11-lem3 37567 wl-ax11-lem8 37572 2sb5ndVD 44907 e2ebindVD 44909 e2ebindALT 44926 2sb5ndALT 44929 |
Copyright terms: Public domain | W3C validator |