**Description:** Equality deduction for class difference. (Contributed by FL, 29-May-2014)

Ref | Expression | ||
---|---|---|---|

Hypotheses | difeq12d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

difeq12d.2 | $${\u22a2}{\phi}\to {C}={D}$$ | ||

Assertion | difeq12d | $${\u22a2}{\phi}\to {A}\setminus {C}={B}\setminus {D}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | difeq12d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

2 | difeq12d.2 | $${\u22a2}{\phi}\to {C}={D}$$ | |

3 | 1 | difeq1d | $${\u22a2}{\phi}\to {A}\setminus {C}={B}\setminus {C}$$ |

4 | 2 | difeq2d | $${\u22a2}{\phi}\to {B}\setminus {C}={B}\setminus {D}$$ |

5 | 3 4 | eqtrd | $${\u22a2}{\phi}\to {A}\setminus {C}={B}\setminus {D}$$ |