# 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 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}$

### Proof

Step Hyp Ref Expression
1 ax-c11 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
2 1 pm2.43i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}={y}$
3 equcomi1 ${⊢}{x}={y}\to {y}={x}$
4 3 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}$
5 2 4 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}$