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

Theorem nelne2 2688
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 2495 . . . 4  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
21biimpcd 216 . . 3  |-  ( A  e.  C  ->  ( A  =  B  ->  B  e.  C ) )
32necon3bd 2635 . 2  |-  ( A  e.  C  ->  ( -.  B  e.  C  ->  A  =/=  B ) )
43imp 419 1  |-  ( ( A  e.  C  /\  -.  B  e.  C
)  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725    =/= wne 2598
This theorem is referenced by:  eldmrexrnb  5869  riotaundb  6583  ac5num  7909  infpssrlem4  8178  fpwwe2lem13  8509  cats1un  11782  dprdfadd  15570  dprdcntz2  15588  lbsextlem4  16225  hauscmplem  17461  fileln0  17874  zcld  18836  dvcnvlem  19852  ppinprm  20927  chtnprm  20929  eupap1  21690  rnlogblem  24391  subfacp1lem5  24862  heiborlem6  26516  lindff1  27258  fnchoice  27667  stoweidlem43  27759  afv0nbfvbi  27982  llnle  30252  lplnle  30274  lhpexle1lem  30741  cdleme18b  31026  cdlemg46  31469  cdlemh  31551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431  df-ne 2600
  Copyright terms: Public domain W3C validator