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

Theorem nelne2 2797
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 2539 . . . 4  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21biimpcd 224 . . 3  |-  ( A  e.  C  ->  ( A  =  B  ->  B  e.  C ) )
32necon3bd 2679 . 2  |-  ( A  e.  C  ->  ( -.  B  e.  C  ->  A  =/=  B ) )
43imp 429 1  |-  ( ( A  e.  C  /\  -.  B  e.  C
)  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462  df-ne 2664
This theorem is referenced by:  eldmrexrnb  6028  ac5num  8417  infpssrlem4  8686  fpwwe2lem13  9020  cats1un  12664  dprdfadd  16862  dprdfaddOLD  16869  dprdcntz2  16888  lbsextlem4  17607  lindff1  18650  hauscmplem  19700  fileln0  20114  zcld  21081  dvcnvlem  22140  ppinprm  23182  chtnprm  23184  footex  23831  foot  23832  colperpexlem3  23839  mideulem  23841  lmieu  23855  eupap1  24680  ordtconlem1  27570  rnlogblem  27683  subfacp1lem5  28296  dvtanlem  29669  heiborlem6  29943  fnchoice  31010  stoweidlem43  31371  afv0nbfvbi  31731  elpwdifsn  31791  llnle  34332  lplnle  34354  lhpexle1lem  34821  cdleme18b  35106  cdlemg46  35549  cdlemh  35631
  Copyright terms: Public domain W3C validator