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|\neg \phi \right\}$$

Proof

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