Theorem eldifsnd 4750

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2956   ∖ cdif 3896  {csn 4584

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-sn 4585

This theorem is used by:  elpwdifsn  4752  prproe  4865  pfxchn  18784  chnind  18795  chnrev  18801  isdrng2  20997  isdrng3lem1  21005  isdrng3lem2  21006  drngmcl  21009  r1pid2  26480  preimaaa  26646  angmgm  29397  dfprlng3  29426  irrednzr  33811  fracfld  33870  mxidlirredi  33996  rprmasso2  34058  rprmirredlem  34062  1arithidomlem1  34067  ufdprmidl  34073  1arithufdlem3  34078  1arithufdlem4  34079  dfufd2lem  34081  dfufd2  34082  zringfrac  34086  ply1dg1rt  34112  esplyind  34207  vietadeg1  34210  r1peuqusdeg1  36408  unitscyglem4  43248  resuppsinopn  43414  readvcot  43415  redivvald  43493  domnexpgn0cl  43584  drngmullcan  43586  drngmulrcan  43587  prjspvs  43638  frlmnzcoordsca  43658  prjspnnorm  43661  sqrtnnaa  47912  sqrtnzqaa  47913