Theorem eldifsnd 4731

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

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

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 3432  df-dif 3893  df-sn 4569

This theorem is referenced by:  elpwdifsn  4733  prproe  4849  pfxchn  18570  chnind  18581  chnrev  18587  drngmcl  20721  r1pid2  26140  irrednzr  33329  fracfld  33387  rprmasso2  33604  rprmirredlem  33608  1arithidomlem1  33613  ufdprmidl  33619  1arithufdlem3  33624  1arithufdlem4  33625  dfufd2lem  33627  dfufd2  33628  zringfrac  33632  ply1dg1rt  33658  esplyind  33737  vietadeg1  33740  r1peuqusdeg1  35844  unitscyglem4  42654  resuppsinopn  42812  readvcot  42813  redivvald  42891  domnexpgn0cl  42985  drngmullcan  42987  drngmulrcan  42988  prjspvs  43060