Description: Symmetric difference with the empty class. The empty class is the identity element for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | symdif0 | |- ( A /_\ (/) ) = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-symdif | |- ( A /_\ (/) ) = ( ( A \ (/) ) u. ( (/) \ A ) ) |
|
| 2 | dif0 | |- ( A \ (/) ) = A |
|
| 3 | 0dif | |- ( (/) \ A ) = (/) |
|
| 4 | 2 3 | uneq12i | |- ( ( A \ (/) ) u. ( (/) \ A ) ) = ( A u. (/) ) |
| 5 | un0 | |- ( A u. (/) ) = A |
|
| 6 | 1 4 5 | 3eqtri | |- ( A /_\ (/) ) = A |