**Description:** Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016)

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

Hypotheses | negidd.1 | $${\u22a2}{\phi}\to {A}\in \u2102$$ | |

pncand.2 | $${\u22a2}{\phi}\to {B}\in \u2102$$ | ||

Assertion | subcld | $${\u22a2}{\phi}\to {A}-{B}\in \u2102$$ |

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

1 | negidd.1 | $${\u22a2}{\phi}\to {A}\in \u2102$$ | |

2 | pncand.2 | $${\u22a2}{\phi}\to {B}\in \u2102$$ | |

3 | subcl | $${\u22a2}\left({A}\in \u2102\wedge {B}\in \u2102\right)\to {A}-{B}\in \u2102$$ | |

4 | 1 2 3 | syl2anc | $${\u22a2}{\phi}\to {A}-{B}\in \u2102$$ |