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		vex	$$⊢x\in \mathrm{V}$$
2		eldif	$$⊢x\in \left(\mathrm{V}\setminus A\right)\leftrightarrow \left(x\in \mathrm{V}\wedge \neg x\in A\right)$$
3	1 2	mpbiran	$$⊢x\in \left(\mathrm{V}\setminus A\right)\leftrightarrow \neg x\in A$$
4	3	con2bii	$$⊢x\in A\leftrightarrow \neg x\in \left(\mathrm{V}\setminus A\right)$$
5	1	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)$$
6	4 5	bitr2i	$$⊢\left(x\in \mathrm{V}\wedge \neg x\in \left(\mathrm{V}\setminus A\right)\right)\leftrightarrow x\in A$$
7	6	difeqri	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus A\right)=A$$