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 583	1 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ {𝐶}))

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3908  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-sn 4586

This theorem is referenced by:  prproe  4865  drngmcl  20670  r1pid2  26100  pfxchn  32981  chnind  32983  irrednzr  33217  fracfld  33274  rprmasso2  33490  rprmirredlem  33494  1arithidomlem1  33499  ufdprmidl  33505  1arithufdlem3  33510  1arithufdlem4  33511  dfufd2lem  33513  dfufd2  33514  zringfrac  33518  ply1dg1rt  33541  r1peuqusdeg1  35623  unitscyglem4  42179  resuppsinopn  42344  readvcot  42345  redivvald  42423  domnexpgn0cl  42504  drngmullcan  42506  drngmulrcan  42507  prjspvs  42591