Theorem eldifsnd 4757

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960   ∖ cdif 3903  {csn 4591

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-sn 4592

This theorem is used by:  elpwdifsn  4759  prproe  4872  pfxchn  18690  chnind  18701  chnrev  18707  isdrng3lem1  20903  isdrng3lem2  20904  drngmcl  20907  r1pid2  26372  dfprlng3  29255  irrednzr  33636  fracfld  33695  mxidlirredi  33820  rprmasso2  33882  rprmirredlem  33886  1arithidomlem1  33891  ufdprmidl  33897  1arithufdlem3  33902  1arithufdlem4  33903  dfufd2lem  33905  dfufd2  33906  zringfrac  33910  ply1dg1rt  33936  esplyind  34031  vietadeg1  34034  r1peuqusdeg1  36174  unitscyglem4  43025  resuppsinopn  43184  readvcot  43185  redivvald  43263  domnexpgn0cl  43351  drngmullcan  43353  drngmulrcan  43354  prjspvs  43402  sqrtnzqaa  47665