Theorem eldifsnd 4763

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932   ∖ cdif 3923  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-sn 4602

This theorem is referenced by:  prproe  4881  drngmcl  20710  r1pid2  26119  pfxchn  32989  chnind  32991  irrednzr  33245  fracfld  33302  rprmasso2  33541  rprmirredlem  33545  1arithidomlem1  33550  ufdprmidl  33556  1arithufdlem3  33561  1arithufdlem4  33562  dfufd2lem  33564  dfufd2  33565  zringfrac  33569  ply1dg1rt  33592  r1peuqusdeg1  35665  unitscyglem4  42211  resuppsinopn  42406  readvcot  42407  domnexpgn0cl  42546  drngmullcan  42548  drngmulrcan  42549  prjspvs  42633