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		uncom	$$⊢\varnothing \cup \left(\mathrm{V}\setminus A\right)=\left(\mathrm{V}\setminus A\right)\cup \varnothing$$
7		un0	$$⊢\left(\mathrm{V}\setminus A\right)\cup \varnothing =\mathrm{V}\setminus A$$
8	6 7	eqtri	$$⊢\varnothing \cup \left(\mathrm{V}\setminus A\right)=\mathrm{V}\setminus A$$
9	5 8	eqtri	$$⊢\left(A\setminus \mathrm{V}\right)\cup \left(\mathrm{V}\setminus A\right)=\mathrm{V}\setminus A$$
10	1 9	eqtri	$$⊢\left(A∆\mathrm{V}\right)=\mathrm{V}\setminus A$$