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		vex	$$⊢x\in \mathrm{V}$$
2		eldif	$$⊢x\in \left(\mathrm{V}\setminus B\right)\leftrightarrow \left(x\in \mathrm{V}\wedge \neg x\in B\right)$$
3	1 2	mpbiran	$$⊢x\in \left(\mathrm{V}\setminus B\right)\leftrightarrow \neg x\in B$$
4	3	con2bii	$$⊢x\in B\leftrightarrow \neg x\in \left(\mathrm{V}\setminus B\right)$$
5	4	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)$$
6		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)$$
7	5 6	bitr4i	$$⊢\left(x\in A\wedge x\in B\right)\leftrightarrow x\in \left(A\setminus \left(\mathrm{V}\setminus B\right)\right)$$
8	7	ineqri	$$⊢A\cap B=A\setminus \left(\mathrm{V}\setminus B\right)$$