Theorem eldifsnd 4746

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ≠ wne 2955   ∖ cdif 4044  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 4046  df-sn 4585

This theorem is used by:  elpwdifsn  4748  prproe  4832  pfxchn  18793  chnind  18804  chnrev  18810  isdrng2  21006  isdrng3lem1  21014  isdrng3lem2  21015  drngmcl  21018  r1pid2  26489  preimaaa  26655  qaa  26656  angmgm  29406  dfprlng3  29435  irrednzr  33861  fracfld  33920  mxidlirredi  34046  rprmasso2  34108  rprmirredlem  34112  1arithidomlem1  34117  ufdprmidl  34123  1arithufdlem3  34128  1arithufdlem4  34129  dfufd2lem  34131  dfufd2  34132  zringfrac  34136  ply1dg1rt  34162  esplyind  34257  vietadeg1  34260  r1peuqusdeg1  36526  unitscyglem4  43385  resuppsinopn  43551  readvcot  43552  redivvald  43630  domnexpgn0cl  43721  drngmullcan  43723  drngmulrcan  43724  prjspvs  43775  frlmnzcoordsca  43795  prjspnnorm  43798  sqrtnnaa  48049  sqrtnzqaa  48050