This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ B
eldifsnd.2 ⊢ φ → A ≠ C
Assertion eldifsnd ⊢ φ → A ∈ B ∖ C

Proof

Step Hyp Ref Expression
1 eldifsnd.1 ⊢ φ → A ∈ B
2 eldifsnd.2 ⊢ φ → A ≠ C
3 eldifsn ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ A ≠ C
4 1 2 3 sylanbrc ⊢ φ → A ∈ B ∖ C