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

Theorem nelne2 2549
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 2356 . . . 4  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21biimpcd 215 . . 3  |-  ( A  e.  C  ->  ( A  =  B  ->  B  e.  C ) )
32necon3bd 2496 . 2  |-  ( A  e.  C  ->  ( -.  B  e.  C  ->  A  =/=  B ) )
43imp 418 1  |-  ( ( A  e.  C  /\  -.  B  e.  C
)  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459
This theorem is referenced by:  riotaundb  6362  ac5num  7679  infpssrlem4  7948  fpwwe2lem13  8280  cats1un  11492  dprdfadd  15271  dprdcntz2  15289  lbsextlem4  15930  hauscmplem  17149  fileln0  17561  zcld  18335  dvcnvlem  19339  ppinprm  20406  chtnprm  20408  rnlogblem  23416  subfacp1lem5  23730  eupap1  23915  topnem  25615  npmp  25624  heiborlem6  26643  lindff1  27393  fnchoice  27803  stoweidlem43  27895  afv0nbfvbi  28119  llnle  30329  lplnle  30351  lhpexle1lem  30818  cdleme18b  31103  cdlemg46  31546  cdlemh  31628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292  df-ne 2461
  Copyright terms: Public domain W3C validator