Theorem eldifsnd

Description: Membership in a set with an element removed : deduction version. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	eldifsnd.1	|- ( ph -> A e. B )
	eldifsnd.2	|- ( ph -> A =/= C )
Assertion	eldifsnd	|- ( ph -> A e. ( B \ { C } ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsnd.1	|- ( ph -> A e. B )
2		eldifsnd.2	|- ( ph -> A =/= C )
3		eldifsn	|- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
4	1 2 3	sylanbrc	|- ( ph -> A e. ( B \ { C } ) )