Theorem neldif

Description: Implication of membership in a class difference. (Contributed by NM, 28-Jun-1994)

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

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
2	1	simplbi2	|- ( A e. B -> ( -. A e. C -> A e. ( B \ C ) ) )
3	2	con1d	|- ( A e. B -> ( -. A e. ( B \ C ) -> A e. C ) )
4	3	imp	|- ( ( A e. B /\ -. A e. ( B \ C ) ) -> A e. C )