Theorem dfin2

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 . Another version is given by dfin4 . (Contributed by NM, 10-Jun-2004)

	Ref	Expression
Assertion	dfin2	$$⊢A\cap B=A\setminus \left(\mathrm{V}\setminus B\right)$$

Proof

Step	Hyp	Ref	Expression
1		velcomp	$$⊢x\in \left(\mathrm{V}\setminus B\right)\leftrightarrow \neg x\in B$$
2	1	con2bii	$$⊢x\in B\leftrightarrow \neg x\in \left(\mathrm{V}\setminus B\right)$$
3	2	anbi2i	$$⊢\left(x\in A\wedge x\in B\right)\leftrightarrow \left(x\in A\wedge \neg x\in \left(\mathrm{V}\setminus B\right)\right)$$
4		eldif	$$⊢x\in \left(A\setminus \left(\mathrm{V}\setminus B\right)\right)\leftrightarrow \left(x\in A\wedge \neg x\in \left(\mathrm{V}\setminus B\right)\right)$$
5	3 4	bitr4i	$$⊢\left(x\in A\wedge x\in B\right)\leftrightarrow x\in \left(A\setminus \left(\mathrm{V}\setminus B\right)\right)$$
6	5	ineqri	$$⊢A\cap B=A\setminus \left(\mathrm{V}\setminus B\right)$$