Theorem eldifsnd 4747

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

Syntax hints:   → wi 4   ∈ wcel 2142   ≠ wne 2957   ∖ cdif 3901  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-sn 4583

This theorem is referenced by:  elpwdifsn  4749  prproe  4863  pfxchn  18642  chnind  18653  chnrev  18659  drngmcl  20800  r1pid2  26222  irrednzr  33431  fracfld  33495  mxidlirredi  33659  rprmasso2  33722  rprmirredlem  33726  1arithidomlem1  33731  ufdprmidl  33737  1arithufdlem3  33742  1arithufdlem4  33743  dfufd2lem  33745  dfufd2  33746  zringfrac  33750  ply1dg1rt  33776  esplyind  33872  vietadeg1  33875  r1peuqusdeg1  35993  unitscyglem4  42815  resuppsinopn  42972  readvcot  42973  redivvald  43051  domnexpgn0cl  43141  drngmullcan  43143  drngmulrcan  43144  prjspvs  43192