Theorem axc11n 2458

Description: Derive set.mm's original ax-c11n 39662 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 2087. Use aecom 2459 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2404. (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 2412	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))
2	1	com12 33	. . . 4 ⊢ (𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑥 = 𝑧))
3		axc11r 2400	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))
4		aev 2089	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)
5	3, 4	syl6 36	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))
6	2, 5	syl9 78	. . 3 ⊢ (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))
7		ax6evr 2045	. . 3 ⊢ ∃𝑧 𝑥 = 𝑧
8	6, 7	exlimiiv 1961	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))
9	8	pm2.18d 128	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-12 2213  ax-13 2404

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814

This theorem is referenced by:  aecom  2459  axi10  2732  wl-hbae1  38174  2sb5ndVD  45618  e2ebindVD  45620  e2ebindALT  45637  2sb5ndALT  45640