Description: The union of a class and its complement is the universe. Theorem 5.1(5) of Stoll p. 17. (Contributed by NM, 17-Aug-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | unvdif | |- ( A u. ( _V \ A ) ) = _V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfun3 | |- ( A u. ( _V \ A ) ) = ( _V \ ( ( _V \ A ) i^i ( _V \ ( _V \ A ) ) ) ) |
|
2 | disjdif | |- ( ( _V \ A ) i^i ( _V \ ( _V \ A ) ) ) = (/) |
|
3 | 2 | difeq2i | |- ( _V \ ( ( _V \ A ) i^i ( _V \ ( _V \ A ) ) ) ) = ( _V \ (/) ) |
4 | dif0 | |- ( _V \ (/) ) = _V |
|
5 | 1 3 4 | 3eqtri | |- ( A u. ( _V \ A ) ) = _V |