Theorem compeq

Description: Equality between two ways of saying "the complement of A ". (Contributed by Andrew Salmon, 15-Jul-2011)

	Ref	Expression
Assertion	compeq	$$⊢\mathrm{V}\setminus A=\left\{x|\neg x\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		velcomp	$$⊢x\in \left(\mathrm{V}\setminus A\right)\leftrightarrow \neg x\in A$$
2	1	abbi2i	$$⊢\mathrm{V}\setminus A=\left\{x|\neg x\in A\right\}$$