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 i^i B ) = ( A \ ( _V \ B ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		eldif	|- ( x e. ( _V \ B ) <-> ( x e. _V /\ -. x e. B ) )
3	1 2	mpbiran	|- ( x e. ( _V \ B ) <-> -. x e. B )
4	3	con2bii	|- ( x e. B <-> -. x e. ( _V \ B ) )
5	4	anbi2i	|- ( ( x e. A /\ x e. B ) <-> ( x e. A /\ -. x e. ( _V \ B ) ) )
6		eldif	|- ( x e. ( A \ ( _V \ B ) ) <-> ( x e. A /\ -. x e. ( _V \ B ) ) )
7	5 6	bitr4i	|- ( ( x e. A /\ x e. B ) <-> x e. ( A \ ( _V \ B ) ) )
8	7	ineqri	|- ( A i^i B ) = ( A \ ( _V \ B ) )