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

Theorem neldifsnd 4460
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 4459 . 2 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
21a1i 11 1 (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2131  cdif 3704  {csn 4313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-v 3334  df-dif 3710  df-sn 4314
This theorem is referenced by:  difsnb  4474  fsnunf2  6608  rpnnen2lem9  15142  fprodfvdvdsd  15252  ramub1lem1  15924  ramub1lem2  15925  prmdvdsprmo  15940  acsfiindd  17370  gsummgp0  18800  islindf4  20371  gsummatr01lem3  20657  nbgrnself  26446  omsmeas  30686  onint1  32746  poimirlem30  33744  prtlem80  34642  gneispace0nelrn3  38934  supminfxr2  40189  fsumnncl  40298  fsumsplit1  40299  hoidmv1lelem2  41304  hspmbllem1  41338  hspmbllem2  41339  fsumsplitsndif  41845  mgpsumunsn  42642
  Copyright terms: Public domain W3C validator