theorem elcpl (A: set) (a: nat): $ a e. Compl A <-> ~a e. A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 | x = a -> (x e. A <-> a e. A) |
|
| 2 | 1 | noteqd | x = a -> (~x e. A <-> ~a e. A) |
| 3 | 2 | elabe | a e. {x | ~x e. A} <-> ~a e. A |
| 4 | 3 | conv Compl | a e. Compl A <-> ~a e. A |