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

Theorem neldifsnd 4793
Description: The class 𝐴 is not in (𝐵 ∖ {𝐴}). Deduction form. (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
neldifsnd (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))

Proof of Theorem neldifsnd
StepHypRef Expression
1 neldifsn 4792 . 2 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
21a1i 11 1 (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2108  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:  difsnb  4806  fsnunf2  7206  fsumsplit1  15781  rpnnen2lem9  16258  fprodfvdvdsd  16371  ramub1lem1  17064  ramub1lem2  17065  prmdvdsprmo  17080  acsfiindd  18598  gsummgp0  20315  islindf4  21858  gsummatr01lem3  22663  nbgrnself  29376  omsmeas  34325  onint1  36450  bj-fvsnun2  37257  poimirlem30  37657  prtlem80  38862  aks6d1c5lem3  42138  gneispace0nelrn3  44155  supminfxr2  45480  fsumnncl  45587  hoidmv1lelem2  46607  hspmbllem1  46641  hspmbllem2  46642  fsumsplitsndif  47360  isubgr3stgrlem3  47935  mgpsumunsn  48277
  Copyright terms: Public domain W3C validator