This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∪ V ∖ A = V

Proof

Step Hyp Ref Expression
1 dfun3 ⊢ A ∪ V ∖ A = V ∖ V ∖ A ∩ V ∖ V ∖ A
2 disjdif ⊢ V ∖ A ∩ V ∖ V ∖ A = ∅
3 2 difeq2i ⊢ V ∖ V ∖ A ∩ V ∖ V ∖ A = V ∖ ∅
4 dif0 ⊢ V ∖ ∅ = V
5 1 3 4 3eqtri ⊢ A ∪ V ∖ A = V