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

Metamath Proof Explorer

Theorem aecom

Description: Commutation law for identical variable specifiers. Both sides of the biconditional are true when x and y are substituted with the same variable. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 10-May-1993) Change to a biconditional. (Revised by BJ, 26-Sep-2019) (New usage is discouraged.)

		Ref	Expression
	Assertion	aecom	⊢ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑦 𝑦 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		axc11n	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )
2		axc11n	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑥 𝑥 = 𝑦 )
3	1 2	impbii	⊢ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑦 𝑦 = 𝑥 )