Theorem eldifsnd 4759

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964   ∖ cdif 3910  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3465  df-dif 3916  df-sn 4595

This theorem is referenced by:  elpwdifsn  4761  prproe  4874  pfxchn  18666  chnind  18677  chnrev  18683  drngmcl  20834  r1pid2  26288  irrednzr  33511  fracfld  33572  mxidlirredi  33699  rprmasso2  33761  rprmirredlem  33765  1arithidomlem1  33770  ufdprmidl  33776  1arithufdlem3  33781  1arithufdlem4  33782  dfufd2lem  33784  dfufd2  33785  zringfrac  33789  ply1dg1rt  33815  esplyind  33910  vietadeg1  33913  r1peuqusdeg1  36034  unitscyglem4  42855  resuppsinopn  43014  readvcot  43015  redivvald  43093  domnexpgn0cl  43183  drngmullcan  43185  drngmulrcan  43186  prjspvs  43234