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	|- ( _V \ ( _V \ A ) ) = A

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		eldif	|- ( x e. ( _V \ A ) <-> ( x e. _V /\ -. x e. A ) )
3	1 2	mpbiran	|- ( x e. ( _V \ A ) <-> -. x e. A )
4	3	con2bii	|- ( x e. A <-> -. x e. ( _V \ A ) )
5	1	biantrur	|- ( -. x e. ( _V \ A ) <-> ( x e. _V /\ -. x e. ( _V \ A ) ) )
6	4 5	bitr2i	|- ( ( x e. _V /\ -. x e. ( _V \ A ) ) <-> x e. A )
7	6	difeqri	|- ( _V \ ( _V \ A ) ) = A