Theorem eldifsnd 4812

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2946   ∖ cdif 3973  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-sn 4649

This theorem is referenced by:  prproe  4929  drngmcl  20772  r1pid2  26221  pfxchn  32982  chnind  32983  irrednzr  33222  fracfld  33275  rprmasso2  33519  rprmirredlem  33523  1arithidomlem1  33528  ufdprmidl  33534  1arithufdlem3  33539  1arithufdlem4  33540  dfufd2lem  33542  dfufd2  33543  zringfrac  33547  ply1dg1rt  33569  r1peuqusdeg1  35611  unitscyglem4  42155  domnexpgn0cl  42478  drngmullcan  42480  drngmulrcan  42481  prjspvs  42565