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		velcomp	|- ( x e. ( _V \ B ) <-> -. x e. B )
2	1	con2bii	|- ( x e. B <-> -. x e. ( _V \ B ) )
3	2	anbi2i	|- ( ( x e. A /\ x e. B ) <-> ( x e. A /\ -. x e. ( _V \ B ) ) )
4		eldif	|- ( x e. ( A \ ( _V \ B ) ) <-> ( x e. A /\ -. x e. ( _V \ B ) ) )
5	3 4	bitr4i	|- ( ( x e. A /\ x e. B ) <-> x e. ( A \ ( _V \ B ) ) )
6	5	ineqri	|- ( A i^i B ) = ( A \ ( _V \ B ) )