This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aecom-o

Description: Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in Megill p. 445 (p. 12 of the preprint). Version of aecom using ax-c11 . Unlike axc11nfromc11 , this version does not require ax-5 (see comment of equcomi1 ). (Contributed by NM, 10-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	aecom-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		ax-c11	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑥 = 𝑦 ) )
2	1	pm2.43i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑥 = 𝑦 )
3		equcomi1	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )
4	3	alimi	⊢ ( ∀ 𝑦 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )
5	2 4	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )