# Metamath Proof Explorer

## Theorem compab

Description: Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion compab ${⊢}\mathrm{V}\setminus \left\{{z}|{\phi }\right\}=\left\{{z}|¬{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\mathrm{V}$
2 nfab1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left\{{z}|{\phi }\right\}$
3 1 2 nfdif ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{V}\setminus \left\{{z}|{\phi }\right\}\right)$
4 nfab1 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left\{{z}|¬{\phi }\right\}$
5 3 4 cleqf ${⊢}\mathrm{V}\setminus \left\{{z}|{\phi }\right\}=\left\{{z}|¬{\phi }\right\}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \left(\mathrm{V}\setminus \left\{{z}|{\phi }\right\}\right)↔{z}\in \left\{{z}|¬{\phi }\right\}\right)$
6 abid ${⊢}{z}\in \left\{{z}|{\phi }\right\}↔{\phi }$
7 6 notbii ${⊢}¬{z}\in \left\{{z}|{\phi }\right\}↔¬{\phi }$
8 velcomp ${⊢}{z}\in \left(\mathrm{V}\setminus \left\{{z}|{\phi }\right\}\right)↔¬{z}\in \left\{{z}|{\phi }\right\}$
9 abid ${⊢}{z}\in \left\{{z}|¬{\phi }\right\}↔¬{\phi }$
10 7 8 9 3bitr4i ${⊢}{z}\in \left(\mathrm{V}\setminus \left\{{z}|{\phi }\right\}\right)↔{z}\in \left\{{z}|¬{\phi }\right\}$
11 5 10 mpgbir ${⊢}\mathrm{V}\setminus \left\{{z}|{\phi }\right\}=\left\{{z}|¬{\phi }\right\}$