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\cup \left(\mathrm{V}\setminus A\right)=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dfun3	$$⊢A\cup \left(\mathrm{V}\setminus A\right)=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)\right)\right)$$
2		disjdif	$$⊢\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)\right)=\varnothing$$
3	2	difeq2i	$$⊢\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)\right)\right)=\mathrm{V}\setminus \varnothing$$
4		dif0	$$⊢\mathrm{V}\setminus \varnothing =\mathrm{V}$$
5	1 3 4	3eqtri	$$⊢A\cup \left(\mathrm{V}\setminus A\right)=\mathrm{V}$$