Theorem eldifsnd 4741

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930   ∖ cdif 3896  {csn 4578

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-v 3440  df-dif 3902  df-sn 4579

This theorem is referenced by:  prproe  4859  pfxchn  18531  chnind  18542  chnrev  18548  drngmcl  20681  r1pid2  26121  irrednzr  33281  fracfld  33339  rprmasso2  33556  rprmirredlem  33560  1arithidomlem1  33565  ufdprmidl  33571  1arithufdlem3  33576  1arithufdlem4  33577  dfufd2lem  33579  dfufd2  33580  zringfrac  33584  ply1dg1rt  33610  esplyind  33680  vietadeg1  33683  r1peuqusdeg1  35786  unitscyglem4  42391  resuppsinopn  42560  readvcot  42561  redivvald  42639  domnexpgn0cl  42720  drngmullcan  42722  drngmulrcan  42723  prjspvs  42795