Theorem eldifsnd 4791

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

Hypotheses

Ref	Expression
eldifsnd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eldifsnd.2	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Assertion

Ref	Expression
eldifsnd	⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ {𝐶}))

Proof of Theorem eldifsnd

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2937   ∖ cdif 3959  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-sn 4631

This theorem is referenced by:  prproe  4909  drngmcl  20766  r1pid2  26215  pfxchn  32983  chnind  32984  irrednzr  33236  fracfld  33289  rprmasso2  33533  rprmirredlem  33537  1arithidomlem1  33542  ufdprmidl  33548  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  dfufd2  33557  zringfrac  33561  ply1dg1rt  33583  r1peuqusdeg1  35627  unitscyglem4  42179  domnexpgn0cl  42509  drngmullcan  42511  drngmulrcan  42512  prjspvs  42596