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

Theorem nelne1 2783
Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
Assertion
Ref Expression
nelne1  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  B  =/=  C )

Proof of Theorem nelne1
StepHypRef Expression
1 eleq2 2527 . . . 4  |-  ( B  =  C  ->  ( A  e.  B  <->  A  e.  C ) )
21biimpcd 224 . . 3  |-  ( A  e.  B  ->  ( B  =  C  ->  A  e.  C ) )
32necon3bd 2666 . 2  |-  ( A  e.  B  ->  ( -.  A  e.  C  ->  B  =/=  C ) )
43imp 427 1  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449  df-ne 2651
This theorem is referenced by:  elnelne1  2801  difsnb  4158  fofinf1o  7793  fin23lem24  8693  fin23lem31  8714  ttukeylem7  8886  npomex  9363  lbspss  17926  islbs3  17999  lbsextlem4  18005  obslbs  18937  hauspwpwf1  20657  ppiltx  23652  tglineneq  24228  lnopp2hpgb  24336  ex-pss  25354  cntnevol  28439  fin2solem  30282  rpnnen3lem  31215  lvecpsslmod  33381  lshpnelb  35125  osumcllem10N  36105  pexmidlem7N  36116  dochsnkrlem1  37612
  Copyright terms: Public domain W3C validator