Theorem notab

Description: A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010)

	Ref	Expression
Assertion	notab	$$⊢\left\{x|\neg \phi \right\}=\mathrm{V}\setminus \left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in \mathrm{V}|\neg \phi \right\}=\left\{x|\left(x\in \mathrm{V}\wedge \neg \phi \right)\right\}$$
2		rabab	$$⊢\left\{x\in \mathrm{V}|\neg \phi \right\}=\left\{x|\neg \phi \right\}$$
3	1 2	eqtr3i	$$⊢\left\{x|\left(x\in \mathrm{V}\wedge \neg \phi \right)\right\}=\left\{x|\neg \phi \right\}$$
4		difab	$$⊢\left\{x|x\in \mathrm{V}\right\}\setminus \left\{x|\phi \right\}=\left\{x|\left(x\in \mathrm{V}\wedge \neg \phi \right)\right\}$$
5		abid2	$$⊢\left\{x|x\in \mathrm{V}\right\}=\mathrm{V}$$
6	5	difeq1i	$$⊢\left\{x|x\in \mathrm{V}\right\}\setminus \left\{x|\phi \right\}=\mathrm{V}\setminus \left\{x|\phi \right\}$$
7	4 6	eqtr3i	$$⊢\left\{x|\left(x\in \mathrm{V}\wedge \neg \phi \right)\right\}=\mathrm{V}\setminus \left\{x|\phi \right\}$$
8	3 7	eqtr3i	$$⊢\left\{x|\neg \phi \right\}=\mathrm{V}\setminus \left\{x|\phi \right\}$$