Theorem eldifsnd 4753

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2957   ∖ cdif 3899  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-sn 4588

This theorem is used by:  elpwdifsn  4755  prproe  4868  pfxchn  18702  chnind  18713  chnrev  18719  isdrng3lem1  20915  isdrng3lem2  20916  drngmcl  20919  r1pid2  26389  dfprlng3  29291  irrednzr  33677  fracfld  33736  mxidlirredi  33861  rprmasso2  33923  rprmirredlem  33927  1arithidomlem1  33932  ufdprmidl  33938  1arithufdlem3  33943  1arithufdlem4  33944  dfufd2lem  33946  dfufd2  33947  zringfrac  33951  ply1dg1rt  33977  esplyind  34072  vietadeg1  34075  r1peuqusdeg1  36209  unitscyglem4  43051  resuppsinopn  43225  readvcot  43226  redivvald  43304  domnexpgn0cl  43392  drngmullcan  43394  drngmulrcan  43395  prjspvs  43443  sqrtnnaa  47718  sqrtnzqaa  47719