Theorem nelne1 2786

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

Assertion

Ref	Expression
nelne1

Proof of Theorem nelne1

Step	Hyp	Ref	Expression
1		eleq2 2530	. . . 4
2	1	biimpcd 224	. . 3
3	2	necon3bd 2669	. 2
4	3	imp 429	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652

This theorem is referenced by:  elnelne1  2804  difsnb  4172  fofinf1o  7821  fin23lem24  8723  fin23lem31  8744  ttukeylem7  8916  npomex  9395  lbspss  17728  islbs3  17801  lbsextlem4  17807  obslbs  18761  hauspwpwf1  20488  ppiltx  23451  tglineneq  24024  lnopp2hpgb  24132  ex-pss  25149  cntnevol  28199  fin2solem  30039  rpnnen3lem  30973  lvecpsslmod  33108  lshpnelb  34709  osumcllem10N  35689  pexmidlem7N  35700  dochsnkrlem1  37196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-ne 2654