Theorem eldifsnd 4755

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 4753	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
4	1, 2, 3	sylanbrc 594	1 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ {𝐶}))

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958   ∖ cdif 3902  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3908  df-sn 4590

This theorem is referenced by:  elpwdifsn  4757  prproe  4870  pfxchn  18661  chnind  18672  chnrev  18678  isdrng3lem1  20851  isdrng3lem2  20852  drngmcl  20855  r1pid2  26319  dfprlng3  29198  irrednzr  33570  fracfld  33629  mxidlirredi  33754  rprmasso2  33816  rprmirredlem  33820  1arithidomlem1  33825  ufdprmidl  33831  1arithufdlem3  33836  1arithufdlem4  33837  dfufd2lem  33839  dfufd2  33840  zringfrac  33844  ply1dg1rt  33870  esplyind  33965  vietadeg1  33968  r1peuqusdeg1  36135  unitscyglem4  42985  resuppsinopn  43144  readvcot  43145  redivvald  43223  domnexpgn0cl  43311  drngmullcan  43313  drngmulrcan  43314  prjspvs  43362  sqrtnzqaa  47625