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

Theorem nelne2 2784
Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
Assertion
Ref Expression
nelne2  |-  ( ( A  e.  C  /\  -.  B  e.  C
)  ->  A  =/=  B )

Proof of Theorem nelne2
StepHypRef Expression
1 eleq1 2526 . . . 4  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21biimpcd 224 . . 3  |-  ( A  e.  C  ->  ( A  =  B  ->  B  e.  C ) )
32necon3bd 2666 . 2  |-  ( A  e.  C  ->  ( -.  B  e.  C  ->  A  =/=  B ) )
43imp 427 1  |-  ( ( A  e.  C  /\  -.  B  e.  C
)  ->  A  =/=  B )
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-5 1709  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:  elnelne2  2802  ac5num  8408  infpssrlem4  8677  fpwwe2lem13  9009  zgt1rpn0n1  11258  cats1un  12695  dprdfadd  17258  dprdfaddOLD  17265  dprdcntz2  17284  lbsextlem4  18005  lindff1  19025  hauscmplem  20076  fileln0  20520  zcld  21487  dvcnvlem  22546  ppinprm  23627  chtnprm  23629  footex  24299  foot  24300  colperpexlem3  24310  mideulem2  24312  opphllem  24313  opphllem2  24324  lnopp2hpgb  24336  lmieu  24354  eupap1  25181  ordtconlem1  28144  esum2dlem  28324  subfacp1lem5  28895  dvtanlem  30307  heiborlem6  30555  bcc0  31489  fnchoice  31647  stoweidlem43  32067  zneoALTV  32583  elpwdifsn  32689  llnle  35658  lplnle  35680  lhpexle1lem  36147  cdleme18b  36433  cdlemg46  36877  cdlemh  36959
  Copyright terms: Public domain W3C validator