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

Theorem nelne2 2536
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 2343 . . . 4  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21biimpcd 215 . . 3  |-  ( A  e.  C  ->  ( A  =  B  ->  B  e.  C ) )
32necon3bd 2483 . 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 1623    e. wcel 1684    =/= wne 2446
This theorem is referenced by:  riotaundb  6346  ac5num  7663  infpssrlem4  7932  fpwwe2lem13  8264  cats1un  11476  dprdfadd  15255  dprdcntz2  15273  lbsextlem4  15914  hauscmplem  17133  fileln0  17545  zcld  18319  dvcnvlem  19323  ppinprm  20390  chtnprm  20392  rnlogblem  23401  subfacp1lem5  23715  eupap1  23900  topnem  25512  npmp  25521  heiborlem6  26540  lindff1  27290  fnchoice  27700  stoweidlem43  27792  afv0nbfvbi  28014  llnle  29707  lplnle  29729  lhpexle1lem  30196  cdleme18b  30481  cdlemg46  30924  cdlemh  31006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279  df-ne 2448
  Copyright terms: Public domain W3C validator