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