![]() |
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 38222 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 2057. Use aecom 2425 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2378 | . . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) | |
2 | 1 | com12 32 | . . . 4 ⊢ (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧)) |
3 | axc11r 2364 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)) | |
4 | aev 2059 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) | |
5 | 3, 4 | syl6 35 | . . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)) |
6 | 2, 5 | syl9 77 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))) |
7 | ax6evr 2017 | . . 3 ⊢ ∃𝑧 𝑥 = 𝑧 | |
8 | 6, 7 | exlimiiv 1933 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)) |
9 | 8 | pm2.18d 127 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1538 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-10 2136 ax-12 2170 ax-13 2370 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-nf 1785 |
This theorem is referenced by: aecom 2425 axi10 2699 wl-hbae1 36852 wl-ax11-lem3 36913 wl-ax11-lem8 36918 2sb5ndVD 44134 e2ebindVD 44136 e2ebindALT 44153 2sb5ndALT 44156 |
Copyright terms: Public domain | W3C validator |