Theorem nelne2 2891

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

Step	Hyp	Ref	Expression
1		eleq1 2689	. . . 4 |- ( A = B -> ( A e. C <-> B e. C ) )
2	1	biimpcd 239	. . 3 |- ( A e. C -> ( A = B -> B e. C ) )
3	2	necon3bd 2808	. 2 |- ( A e. C -> ( -. B e. C -> A =/= B ) )
4	3	imp 445	1 |- ( ( A e. C /\ -. B e. C ) -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-ne 2795

This theorem is referenced by:  nelelne  2892  elnelne2  2908  elpwdifsn  4319  ac5num  8859  infpssrlem4  9128  fpwwe2lem13  9464  zgt1rpn0n1  11871  cats1un  13475  dprdfadd  18419  dprdcntz2  18437  lbsextlem4  19161  lindff1  20159  hauscmplem  21209  fileln0  21654  zcld  22616  dvcnvlem  23739  ppinprm  24878  chtnprm  24880  footex  25613  foot  25614  colperpexlem3  25624  mideulem2  25626  opphllem  25627  opphllem2  25640  lnopp2hpgb  25655  colhp  25662  lmieu  25676  trgcopy  25696  trgcopyeulem  25697  ordtconnlem1  29970  esum2dlem  30154  subfacp1lem5  31166  heiborlem6  33615  llnle  34804  lplnle  34826  lhpexle1lem  35293  cdleme18b  35579  cdlemg46  36023  cdlemh  36105  bcc0  38539  fnchoice  39188  climxrre  39982  stoweidlem43  40260  zneoALTV  41580