Theorem eldifsnd 4736

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928   ∖ cdif 3894  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-sn 4574

This theorem is referenced by:  prproe  4854  pfxchn  18516  chnind  18527  chnrev  18533  drngmcl  20665  r1pid2  26094  irrednzr  33217  fracfld  33274  rprmasso2  33491  rprmirredlem  33495  1arithidomlem1  33500  ufdprmidl  33506  1arithufdlem3  33511  1arithufdlem4  33512  dfufd2lem  33514  dfufd2  33515  zringfrac  33519  ply1dg1rt  33543  r1peuqusdeg1  35687  unitscyglem4  42301  resuppsinopn  42466  readvcot  42467  redivvald  42545  domnexpgn0cl  42626  drngmullcan  42628  drngmulrcan  42629  prjspvs  42713