Theorem eldifsnd 4745

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3900  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-sn 4583

This theorem is referenced by:  prproe  4863  pfxchn  18545  chnind  18556  chnrev  18562  drngmcl  20695  r1pid2  26135  irrednzr  33344  fracfld  33402  rprmasso2  33619  rprmirredlem  33623  1arithidomlem1  33628  ufdprmidl  33634  1arithufdlem3  33639  1arithufdlem4  33640  dfufd2lem  33642  dfufd2  33643  zringfrac  33647  ply1dg1rt  33673  esplyind  33752  vietadeg1  33755  r1peuqusdeg1  35859  unitscyglem4  42568  resuppsinopn  42733  readvcot  42734  redivvald  42812  domnexpgn0cl  42893  drngmullcan  42895  drngmulrcan  42896  prjspvs  42968