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

Theorem inelcm 3522
Description: The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
Assertion
Ref Expression
inelcm  |-  ( ( A  e.  B  /\  A  e.  C )  ->  ( B  i^i  C
)  =/=  (/) )

Proof of Theorem inelcm
StepHypRef Expression
1 elin 3371 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
2 ne0i 3474 . 2  |-  ( A  e.  ( B  i^i  C )  ->  ( B  i^i  C )  =/=  (/) )
31, 2sylbir 204 1  |-  ( ( A  e.  B  /\  A  e.  C )  ->  ( B  i^i  C
)  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696    =/= wne 2459    i^i cin 3164   (/)c0 3468
This theorem is referenced by:  minel  3523  disji  4027  disjiun  4029  onnseq  6377  en3lplem1  7432  cplem1  7575  fpwwe2lem12  8279  limsupgre  11971  lmcls  17046  concn  17168  iunconlem  17169  concompclo  17177  2ndcsep  17201  txcls  17315  pthaus  17348  qtopeu  17423  trfbas2  17554  filss  17564  zfbas  17607  fmfnfm  17669  tsmsfbas  17826  qdensere  18295  reperflem  18339  reconnlem1  18347  metds0  18370  metnrmlem1a  18378  minveclem3b  18808  ovolicc2lem5  18896  taylfval  19754  disjif  23370  disjif2  23373  subfacp1lem6  23731  erdszelem5  23741  pconcon  23777  cvmseu  23822  uninqs  25142  lfinpfin  26406  locfincmp  26407  neibastop2lem  26412  sstotbnd3  26603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-in 3172  df-nul 3469
  Copyright terms: Public domain W3C validator