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

Theorem nelne2 2707
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 2503 . . . 4  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21biimpcd 224 . . 3  |-  ( A  e.  C  ->  ( A  =  B  ->  B  e.  C ) )
32necon3bd 2650 . 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 1369    e. wcel 1756    =/= wne 2611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439  df-ne 2613
This theorem is referenced by:  eldmrexrnb  5855  ac5num  8211  infpssrlem4  8480  fpwwe2lem13  8814  cats1un  12375  dprdfadd  16515  dprdfaddOLD  16522  dprdcntz2  16541  lbsextlem4  17247  lindff1  18254  hauscmplem  19014  fileln0  19428  zcld  20395  dvcnvlem  21453  ppinprm  22495  chtnprm  22497  footex  23114  foot  23115  eupap1  23602  ordtconlem1  26359  rnlogblem  26463  subfacp1lem5  27077  dvtanlem  28446  heiborlem6  28720  fnchoice  29756  stoweidlem43  29843  afv0nbfvbi  30062  llnle  33167  lplnle  33189  lhpexle1lem  33656  cdleme18b  33941  cdlemg46  34384  cdlemh  34466
  Copyright terms: Public domain W3C validator