Theorem eldifsnd 4752

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959   ∖ cdif 4048  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-sn 4589

This theorem is used by:  elpwdifsn  4754  prproe  4838  pfxchn  18834  chnind  18845  chnrev  18851  isdrng2  21048  isdrng3lem1  21056  isdrng3lem2  21057  drngmcl  21060  r1pid2  26535  preimaaa  26703  qaa  26704  angmgm  29454  dfprlng3  29483  irrednzr  33910  isedom  33953  edomediv  33955  zzedom  33958  ply1edom  33959  edompidlem  33960  fracfld  33974  mxidlirredi  34100  rprmasso2  34162  rprmirredlem  34166  1arithidomlem1  34171  ufdprmidl  34177  1arithufdlem3  34182  1arithufdlem4  34183  dfufd2lem  34185  dfufd2  34186  zringfrac  34189  ply1dg1rt  34215  esplyind  34318  vietadeg1  34321  r1peuqusdeg1  36616  unitscyglem4  43514  resuppsinopn  43680  readvcot  43681  redivvald  43759  domnexpgn0cl  43850  drngmullcan  43852  drngmulrcan  43853  prjspvs  43904  frlmnzcoordsca  43924  prjspnnorm  43927  sqrtnnaa  48186  sqrtnzqaa  48187  tanhcl  51250