Theorem notrab

Description: Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	notrab	$$⊢A\setminus \left\{x\in A|\phi \right\}=\left\{x\in A|\neg \phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		difab	$$⊢\left\{x|x\in A\right\}\setminus \left\{x|\phi \right\}=\left\{x|\left(x\in A\wedge \neg \phi \right)\right\}$$
2		difin	$$⊢A\setminus \left(A\cap \left\{x|\phi \right\}\right)=A\setminus \left\{x|\phi \right\}$$
3		dfrab3	$$⊢\left\{x\in A|\phi \right\}=A\cap \left\{x|\phi \right\}$$
4	3	difeq2i	$$⊢A\setminus \left\{x\in A|\phi \right\}=A\setminus \left(A\cap \left\{x|\phi \right\}\right)$$
5		abid2	$$⊢\left\{x|x\in A\right\}=A$$
6	5	difeq1i	$$⊢\left\{x|x\in A\right\}\setminus \left\{x|\phi \right\}=A\setminus \left\{x|\phi \right\}$$
7	2 4 6	3eqtr4i	$$⊢A\setminus \left\{x\in A|\phi \right\}=\left\{x|x\in A\right\}\setminus \left\{x|\phi \right\}$$
8		df-rab	$$⊢\left\{x\in A|\neg \phi \right\}=\left\{x|\left(x\in A\wedge \neg \phi \right)\right\}$$
9	1 7 8	3eqtr4i	$$⊢A\setminus \left\{x\in A|\phi \right\}=\left\{x\in A|\neg \phi \right\}$$