Theorem eldifsnd 4751

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

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

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 3449  df-dif 3917  df-sn 4590

This theorem is referenced by:  prproe  4869  drngmcl  20659  r1pid2  26067  pfxchn  32935  chnind  32937  irrednzr  33201  fracfld  33258  rprmasso2  33497  rprmirredlem  33501  1arithidomlem1  33506  ufdprmidl  33512  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  dfufd2  33521  zringfrac  33525  ply1dg1rt  33548  r1peuqusdeg1  35630  unitscyglem4  42186  resuppsinopn  42351  readvcot  42352  redivvald  42430  domnexpgn0cl  42511  drngmullcan  42513  drngmulrcan  42514  prjspvs  42598