Theorem eldifsn

Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007)

	Ref	Expression
Assertion	eldifsn	|- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( B \ { C } ) <-> ( A e. B /\ -. A e. { C } ) )
2		elsng	|- ( A e. B -> ( A e. { C } <-> A = C ) )
3	2	necon3bbid	|- ( A e. B -> ( -. A e. { C } <-> A =/= C ) )
4	3	pm5.32i	|- ( ( A e. B /\ -. A e. { C } ) <-> ( A e. B /\ A =/= C ) )
5	1 4	bitri	|- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )