Theorem eldif

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994)

	Ref	Expression
Assertion	eldif	|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. ( B \ C ) -> A e. _V )
2		elex	|- ( A e. B -> A e. _V )
3	2	adantr	|- ( ( A e. B /\ -. A e. C ) -> A e. _V )
4		eleq1	|- ( x = y -> ( x e. B <-> y e. B ) )
5		eleq1	|- ( x = y -> ( x e. C <-> y e. C ) )
6	5	notbid	|- ( x = y -> ( -. x e. C <-> -. y e. C ) )
7	4 6	anbi12d	|- ( x = y -> ( ( x e. B /\ -. x e. C ) <-> ( y e. B /\ -. y e. C ) ) )
8		eleq1	|- ( y = A -> ( y e. B <-> A e. B ) )
9		eleq1	|- ( y = A -> ( y e. C <-> A e. C ) )
10	9	notbid	|- ( y = A -> ( -. y e. C <-> -. A e. C ) )
11	8 10	anbi12d	|- ( y = A -> ( ( y e. B /\ -. y e. C ) <-> ( A e. B /\ -. A e. C ) ) )
12		df-dif	|- ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
13	7 11 12	elab2gw	|- ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
14	1 3 13	pm5.21nii	|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )