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	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	eldifsnd.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
Assertion	eldifsnd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ { 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsnd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		eldifsnd.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
3		eldifsn	⊢ ( 𝐴 ∈ ( 𝐵 ∖ { 𝐶 } ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ) )
4	1 2 3	sylanbrc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ∖ { 𝐶 } ) )