Theorem axc11n 2456

Description: Derive set.mm's original ax-c11n 39473 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 2076. Use aecom 2457 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2402. (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.

Step	Hyp	Ref	Expression
1		dveeq1 2410	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
2	1	com12 32	. . . 4 ⊢ (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧))
3		axc11r 2398	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
4		aev 2078	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
5	3, 4	syl6 35	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))
6	2, 5	syl9 77	. . 3 ⊢ (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
7		ax6evr 2034	. . 3 ⊢ ∃𝑧 𝑥 = 𝑧
8	6, 7	exlimiiv 1950	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
9	8	pm2.18d 127	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174  ax-12 2211  ax-13 2402

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803

This theorem is referenced by:  aecom  2457  axi10  2730  wl-hbae1  37983  2sb5ndVD  45446  e2ebindVD  45448  e2ebindALT  45465  2sb5ndALT  45468