Theorem nelne1 2890

Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)

Assertion

Ref	Expression
nelne1	|- ( ( A e. B /\ -. A e. C ) -> B =/= C )

Proof of Theorem nelne1

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

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:  elnelne1  2907  difsnb  4337  fofinf1o  8241  fin23lem24  9144  fin23lem31  9165  ttukeylem7  9337  npomex  9818  lbspss  19082  islbs3  19155  lbsextlem4  19161  obslbs  20074  hauspwpwf1  21791  ppiltx  24903  tglineneq  25539  lnopp2hpgb  25655  colopp  25661  ex-pss  27285  unelldsys  30221  cntnevol  30291  fin2solem  33395  lshpnelb  34271  osumcllem10N  35251  pexmidlem7N  35262  dochsnkrlem1  36758  rpnnen3lem  37598  lvecpsslmod  42296