Description: Proof of equcomi from equid1 , avoiding use of ax-5 (the only use of ax-5 is via ax7 , so using ax-7 instead would remove dependency on ax-5 ). (Contributed by BJ, 8-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | equcomi1 | |- ( x = y -> y = x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equid1 | |- x = x |
|
| 2 | ax7 | |- ( x = y -> ( x = x -> y = x ) ) |
|
| 3 | 1 2 | mpi | |- ( x = y -> y = x ) |