Theorem eldifsnd 4750

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955   ∖ cdif 3896  {csn 4584

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-sn 4585

This theorem is used by:  elpwdifsn  4752  prproe  4865  pfxchn  18699  chnind  18710  chnrev  18716  isdrng3lem1  20915  isdrng3lem2  20916  drngmcl  20919  r1pid2  26388  preimaaa  26556  angmgm  29277  dfprlng3  29306  irrednzr  33691  fracfld  33750  mxidlirredi  33875  rprmasso2  33937  rprmirredlem  33941  1arithidomlem1  33946  ufdprmidl  33952  1arithufdlem3  33957  1arithufdlem4  33958  dfufd2lem  33960  dfufd2  33961  zringfrac  33965  ply1dg1rt  33991  esplyind  34086  vietadeg1  34089  r1peuqusdeg1  36223  unitscyglem4  43065  resuppsinopn  43239  readvcot  43240  redivvald  43318  domnexpgn0cl  43406  drngmullcan  43408  drngmulrcan  43409  prjspvs  43457  sqrtnnaa  47732  sqrtnzqaa  47733