Theorem eldifsnbd

Description: Membership in a set with an element removed implies non-equality with that element. (Contributed by Thierry Arnoux, 13-Jul-2026)

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

Proof

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