Metamath Proof Explorer


Theorem ssdif

Description: Difference law for subsets. (Contributed by NM, 28-May-1998)

Ref Expression
Assertion ssdif ABACBC

Proof

Step Hyp Ref Expression
1 ssel ABxAxB
2 1 anim1d ABxA¬xCxB¬xC
3 eldif xACxA¬xC
4 eldif xBCxB¬xC
5 2 3 4 3imtr4g ABxACxBC
6 5 ssrdv ABACBC