MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axc11n Structured version   Visualization version   GIF version

Theorem axc11n 2417
Description: Derive set.mm's original ax-c11n 38262 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 2050. Use aecom 2418 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2363. (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.)
Assertion
Ref Expression
axc11n (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Proof of Theorem axc11n
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 dveeq1 2371 . . . . 5 (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
21com12 32 . . . 4 (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧))
3 axc11r 2357 . . . . 5 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
4 aev 2052 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
53, 4syl6 35 . . . 4 (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))
62, 5syl9 77 . . 3 (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
7 ax6evr 2010 . . 3 𝑧 𝑥 = 𝑧
86, 7exlimiiv 1926 . 2 (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
98pm2.18d 127 1 (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-12 2163  ax-13 2363
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-nf 1778
This theorem is referenced by:  aecom  2418  axi10  2692  wl-hbae1  36889  wl-ax11-lem3  36953  wl-ax11-lem8  36958  2sb5ndVD  44221  e2ebindVD  44223  e2ebindALT  44240  2sb5ndALT  44243
  Copyright terms: Public domain W3C validator