This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Define class difference, also called relative complement. Definition 5.12 of TakeutiZaring p. 20. For example, ( { 1 , 3 } \ { 1 , 8 } ) = { 3 } ( ex-dif ). Contrast this operation with union ( A u. B ) ( df-un ) and intersection ( A i^i B ) ( df-in ). Several notations are used in the literature; we chose the \ convention used in Definition 5.3 of Eisenberg p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology " A excludes B " to mean A \ B . We will use " B is removed from A " to mean A \ { B } i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-dif |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ||
| 1 | cB | ||
| 2 | 0 1 | cdif | |
| 3 | vx | ||
| 4 | 3 | cv | |
| 5 | 4 0 | wcel | |
| 6 | 4 1 | wcel | |
| 7 | 6 | wn | |
| 8 | 5 7 | wa | |
| 9 | 8 3 | cab | |
| 10 | 2 9 | wceq |