![]() |
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 37753 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 2058. Use aecom 2426 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2379 | . . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) | |
2 | 1 | com12 32 | . . . 4 ⊢ (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧)) |
3 | axc11r 2365 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)) | |
4 | aev 2060 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) | |
5 | 3, 4 | syl6 35 | . . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)) |
6 | 2, 5 | syl9 77 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))) |
7 | ax6evr 2018 | . . 3 ⊢ ∃𝑧 𝑥 = 𝑧 | |
8 | 6, 7 | exlimiiv 1934 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)) |
9 | 8 | pm2.18d 127 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-10 2137 ax-12 2171 ax-13 2371 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-nf 1786 |
This theorem is referenced by: aecom 2426 axi10 2700 wl-hbae1 36383 wl-ax11-lem3 36444 wl-ax11-lem8 36449 2sb5ndVD 43661 e2ebindVD 43663 e2ebindALT 43680 2sb5ndALT 43683 |
Copyright terms: Public domain | W3C validator |