Theorem eldifsnd 4743

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2932   ∖ cdif 3898  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-sn 4581

This theorem is referenced by:  prproe  4861  pfxchn  18533  chnind  18544  chnrev  18550  drngmcl  20683  r1pid2  26123  irrednzr  33332  fracfld  33390  rprmasso2  33607  rprmirredlem  33611  1arithidomlem1  33616  ufdprmidl  33622  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  dfufd2  33631  zringfrac  33635  ply1dg1rt  33661  esplyind  33731  vietadeg1  33734  r1peuqusdeg1  35837  unitscyglem4  42452  resuppsinopn  42618  readvcot  42619  redivvald  42697  domnexpgn0cl  42778  drngmullcan  42780  drngmulrcan  42781  prjspvs  42853