Theorem axc11n 2431

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.)

Assertion

Ref	Expression
axc11n	⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Proof of Theorem axc11n

Dummy variable 𝑧 is distinct from all other variables.

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 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

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