Theorem eldifsnd 4732

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2932   ∖ cdif 3886  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-sn 4568

This theorem is referenced by:  elpwdifsn  4734  prproe  4848  pfxchn  18576  chnind  18587  chnrev  18593  drngmcl  20727  r1pid2  26127  irrednzr  33311  fracfld  33369  rprmasso2  33586  rprmirredlem  33590  1arithidomlem1  33595  ufdprmidl  33601  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  dfufd2  33610  zringfrac  33614  ply1dg1rt  33640  esplyind  33719  vietadeg1  33722  r1peuqusdeg1  35825  unitscyglem4  42637  resuppsinopn  42795  readvcot  42796  redivvald  42874  domnexpgn0cl  42968  drngmullcan  42970  drngmulrcan  42971  prjspvs  43043