theorem cpleqd (_G: wff) (_A1 _A2: set): $ _G -> _A1 == _A2 $ > $ _G -> Compl _A1 == Compl _A2 $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp _Ah | _G -> _A1 == _A2 |
|
| 2 | 1 | eleq2d | _G -> (x e. _A1 <-> x e. _A2) |
| 3 | 2 | noteqd | _G -> (~x e. _A1 <-> ~x e. _A2) |
| 4 | 3 | abeqd | _G -> {x | ~x e. _A1} == {x | ~x e. _A2} |
| 5 | 4 | conv Compl | _G -> Compl _A1 == Compl _A2 |