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

Theorem nelne1 2778
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 2525 . . . 4  |-  ( B  =  C  ->  ( A  e.  B  <->  A  e.  C ) )
21biimpcd 224 . . 3  |-  ( A  e.  B  ->  ( B  =  C  ->  A  e.  C ) )
32necon3bd 2661 . 2  |-  ( A  e.  B  ->  ( -.  A  e.  C  ->  B  =/=  C ) )
43imp 429 1  |-  ( ( A  e.  B  /\  -.  A  e.  C
)  ->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758    =/= wne 2645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2444  df-clel 2447  df-ne 2647
This theorem is referenced by:  difsnb  4118  fofinf1o  7698  fin23lem24  8597  fin23lem31  8618  ttukeylem7  8790  npomex  9271  lbspss  17281  islbs3  17354  lbsextlem4  17360  obslbs  18275  hauspwpwf1  19687  ppiltx  22643  tglineneq  23183  ex-pss  23782  cntnevol  26782  fin2solem  28558  rpnnen3lem  29523  lvecpsslmod  31163  lshpnelb  32948  osumcllem10N  33928  pexmidlem7N  33939  dochsnkrlem1  35433
  Copyright terms: Public domain W3C validator