| 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 38889 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 2055. Use aecom 2432 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2377. (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 2385 | . . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) | |
| 2 | 1 | com12 32 | . . . 4 ⊢ (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧)) |
| 3 | axc11r 2371 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)) | |
| 4 | aev 2057 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) | |
| 5 | 3, 4 | syl6 35 | . . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)) |
| 6 | 2, 5 | syl9 77 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))) |
| 7 | ax6evr 2014 | . . 3 ⊢ ∃𝑧 𝑥 = 𝑧 | |
| 8 | 6, 7 | exlimiiv 1931 | . 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 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-12 2177 ax-13 2377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: aecom 2432 axi10 2705 wl-hbae1 37520 wl-ax11-lem3 37588 wl-ax11-lem8 37593 2sb5ndVD 44930 e2ebindVD 44932 e2ebindALT 44949 2sb5ndALT 44952 |
| Copyright terms: Public domain | W3C validator |