Theorem inelcm 3881

Description: The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)

Assertion

Ref	Expression
inelcm

Proof of Theorem inelcm

Step	Hyp	Ref	Expression
1		elin 3686	. 2
2		ne0i 3790	. 2
3	1, 2	sylbir 213	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  =/=wne 2652  i^icin 3474  c0 3784

This theorem is referenced by:  minel  3882  disji  4440  disjiun  4442  onnseq  7034  uniinqs  7410  en3lplem1  8052  cplem1  8328  fpwwe2lem12  9040  swrdn0  12655  limsupgre  13304  lmcls  19803  concn  19927  iunconlem  19928  concompclo  19936  2ndcsep  19960  lfinpfin  20025  locfincmp  20027  txcls  20105  pthaus  20139  qtopeu  20217  trfbas2  20344  filss  20354  zfbas  20397  fmfnfm  20459  tsmsfbas  20626  restmetu  21090  qdensere  21277  reperflem  21323  reconnlem1  21331  metds0  21354  metnrmlem1a  21362  minveclem3b  21843  ovolicc2lem5  21932  taylfval  22754  wwlkm1edg  24735  disjif  27439  disjif2  27442  subfacp1lem6  28629  erdszelem5  28639  pconcon  28676  cvmseu  28721  neibastop2lem  30178  sstotbnd3  30272

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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-in 3482  df-nul 3785