Theorem ddif

Description: Double complement under universal class. Exercise 4.10(s) of Mendelson p. 231. (Contributed by NM, 8-Jan-2002)

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

Proof

Step	Hyp	Ref	Expression
1		velcomp	$$⊢x\in \left(\mathrm{V}\setminus A\right)\leftrightarrow \neg x\in A$$
2	1	con2bii	$$⊢x\in A\leftrightarrow \neg x\in \left(\mathrm{V}\setminus A\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	biantrur	$$⊢\neg x\in \left(\mathrm{V}\setminus A\right)\leftrightarrow \left(x\in \mathrm{V}\wedge \neg x\in \left(\mathrm{V}\setminus A\right)\right)$$
5	2 4	bitr2i	$$⊢\left(x\in \mathrm{V}\wedge \neg x\in \left(\mathrm{V}\setminus A\right)\right)\leftrightarrow x\in A$$
6	5	difeqri	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)=A$$