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

Theorem neldifsnd 4291
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 4290 . 2 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
21a1i 11 1 (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1987  cdif 3552  {csn 4148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3188  df-dif 3558  df-sn 4149
This theorem is referenced by:  difsnb  4306  fsnunf2  6406  rpnnen2lem9  14876  fprodfvdvdsd  14982  ramub1lem1  15654  ramub1lem2  15655  prmdvdsprmo  15670  acsfiindd  17098  gsummgp0  18529  islindf4  20096  gsummatr01lem3  20382  nbgrnself  26144  omsmeas  30166  onint1  32090  poimirlem30  33071  prtlem80  33625  gneispace0nelrn3  37922  fsumnncl  39207  fsumsplit1  39208  hoidmv1lelem2  40113  hspmbllem1  40147  hspmbllem2  40148  fsumsplitsndif  40641  mgpsumunsn  41428
  Copyright terms: Public domain W3C validator