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

Theorem nelsn 4011
Description: If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
nelsn  |-  ( A  =/=  B  ->  -.  A  e.  { B } )

Proof of Theorem nelsn
StepHypRef Expression
1 neneq 2640 . . . 4  |-  ( A  =/=  B  ->  -.  A  =  B )
21adantr 471 . . 3  |-  ( ( A  =/=  B  /\  A  e.  _V )  ->  -.  A  =  B )
3 elsncg 4002 . . . 4  |-  ( A  e.  _V  ->  ( A  e.  { B } 
<->  A  =  B ) )
43adantl 472 . . 3  |-  ( ( A  =/=  B  /\  A  e.  _V )  ->  ( A  e.  { B }  <->  A  =  B
) )
52, 4mtbird 307 . 2  |-  ( ( A  =/=  B  /\  A  e.  _V )  ->  -.  A  e.  { B } )
6 prcnel 3071 . . 3  |-  ( -.  A  e.  _V  ->  -.  A  e.  { B } )
76adantl 472 . 2  |-  ( ( A  =/=  B  /\  -.  A  e.  _V )  ->  -.  A  e.  { B } )
85, 7pm2.61dan 805 1  |-  ( A  =/=  B  ->  -.  A  e.  { B } )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1454    e. wcel 1897    =/= wne 2632   _Vcvv 3056   {csn 3979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-v 3058  df-sn 3980
This theorem is referenced by:  disjf1o  37503  etransc  38186  gsumge0cl  38250  meadjiunlem  38340  hspmbllem2  38486  upgrres1  39429
  Copyright terms: Public domain W3C validator