Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | difeq1i.1 | |- A = B |
|
| Assertion | difeq1i | |- ( A \ C ) = ( B \ C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difeq1i.1 | |- A = B |
|
| 2 | difeq1 | |- ( A = B -> ( A \ C ) = ( B \ C ) ) |
|
| 3 | 1 2 | ax-mp | |- ( A \ C ) = ( B \ C ) |