Theorem eldifsnd 4738

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3900  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-sn 4578

This theorem is referenced by:  prproe  4856  drngmcl  20635  r1pid2  26065  pfxchn  32951  chnind  32953  irrednzr  33190  fracfld  33247  rprmasso2  33463  rprmirredlem  33467  1arithidomlem1  33472  ufdprmidl  33478  1arithufdlem3  33483  1arithufdlem4  33484  dfufd2lem  33486  dfufd2  33487  zringfrac  33491  ply1dg1rt  33515  r1peuqusdeg1  35620  unitscyglem4  42175  resuppsinopn  42340  readvcot  42341  redivvald  42419  domnexpgn0cl  42500  drngmullcan  42502  drngmulrcan  42503  prjspvs  42587