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

Theorem neldifsnd 4758
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 4757 . 2 ¬ 𝐴 ∈ (𝐵 ∖ {𝐴})
21a1i 11 1 (𝜑 → ¬ 𝐴 ∈ (𝐵 ∖ {𝐴}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  cdif 3912  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-v 3450  df-dif 3918  df-sn 4592
This theorem is referenced by:  difsnb  4771  fsnunf2  7137  fsumsplit1  15637  rpnnen2lem9  16111  fprodfvdvdsd  16223  ramub1lem1  16905  ramub1lem2  16906  prmdvdsprmo  16921  acsfiindd  18449  gsummgp0  20039  islindf4  21260  gsummatr01lem3  22022  nbgrnself  28349  omsmeas  32963  onint1  34950  bj-fvsnun2  35756  poimirlem30  36137  prtlem80  37352  gneispace0nelrn3  42488  supminfxr2  43778  fsumnncl  43887  hoidmv1lelem2  44907  hspmbllem1  44941  hspmbllem2  44942  fsumsplitsndif  45639  mgpsumunsn  46511
  Copyright terms: Public domain W3C validator