MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifsnd Structured version   Visualization version   GIF version

Theorem eldifsnd 4787
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
StepHypRef Expression
1 eldifsnd.1 . 2 (𝜑𝐴𝐵)
2 eldifsnd.2 . 2 (𝜑𝐴𝐶)
3 eldifsn 4786 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
41, 2, 3sylanbrc 583 1 (𝜑𝐴 ∈ (𝐵 ∖ {𝐶}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wne 2940  cdif 3948  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-sn 4627
This theorem is referenced by:  prproe  4905  drngmcl  20750  r1pid2  26201  pfxchn  32999  chnind  33001  irrednzr  33254  fracfld  33310  rprmasso2  33554  rprmirredlem  33558  1arithidomlem1  33563  ufdprmidl  33569  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  dfufd2  33578  zringfrac  33582  ply1dg1rt  33604  r1peuqusdeg1  35648  unitscyglem4  42199  resuppsinopn  42393  readvcot  42394  domnexpgn0cl  42533  drngmullcan  42535  drngmulrcan  42536  prjspvs  42620
  Copyright terms: Public domain W3C validator