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	⊢ ( 𝐴 ∪ ( V ∖ 𝐴 ) ) = V

Proof

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