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

Proof

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