Metamath Proof Explorer


Theorem unvdif

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

Proof

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