Theorem symdifv

Description: The symmetric difference with the universal class is the complement. (Contributed by Scott Fenton, 24-Apr-2012)

	Ref	Expression
Assertion	symdifv	$$⊢\left(A∆\mathrm{V}\right)=\mathrm{V}\setminus A$$

Proof

Step	Hyp	Ref	Expression
1		df-symdif	$$⊢\left(A∆\mathrm{V}\right)=\left(A\setminus \mathrm{V}\right)\cup \left(\mathrm{V}\setminus A\right)$$
2		ssv	$$⊢A\subseteq \mathrm{V}$$
3		ssdif0	$$⊢A\subseteq \mathrm{V}\leftrightarrow A\setminus \mathrm{V}=\varnothing$$
4	2 3	mpbi	$$⊢A\setminus \mathrm{V}=\varnothing$$
5	4	uneq1i	$$⊢\left(A\setminus \mathrm{V}\right)\cup \left(\mathrm{V}\setminus A\right)=\varnothing \cup \left(\mathrm{V}\setminus A\right)$$
6		0un	$$⊢\varnothing \cup \left(\mathrm{V}\setminus A\right)=\mathrm{V}\setminus A$$
7	1 5 6	3eqtri	$$⊢\left(A∆\mathrm{V}\right)=\mathrm{V}\setminus A$$