Theorem eldifsnd 4720

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

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2934   ∖ cdif 3880  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-v 3433  df-dif 3886  df-sn 4556

This theorem is referenced by:  elpwdifsn  4722  prproe  4836  pfxchn  18567  chnind  18578  chnrev  18584  drngmcl  20722  r1pid2  26145  irrednzr  33331  fracfld  33392  rprmasso2  33609  rprmirredlem  33613  1arithidomlem1  33618  ufdprmidl  33624  1arithufdlem3  33629  1arithufdlem4  33630  dfufd2lem  33632  dfufd2  33633  zringfrac  33637  ply1dg1rt  33663  esplyind  33759  vietadeg1  33762  r1peuqusdeg1  35871  unitscyglem4  42683  resuppsinopn  42840  readvcot  42841  redivvald  42919  domnexpgn0cl  43009  drngmullcan  43011  drngmulrcan  43012  prjspvs  43060