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 | |- ( A. x x = y <-> A. y y = x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axc11n | |- ( A. x x = y -> A. y y = x ) |
|
| 2 | axc11n | |- ( A. y y = x -> A. x x = y ) |
|
| 3 | 1 2 | impbii | |- ( A. x x = y <-> A. y y = x ) |