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

Theorem inelcm 3684
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 3532 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
2 ne0i 3636 . 2  |-  ( A  e.  ( B  i^i  C )  ->  ( B  i^i  C )  =/=  (/) )
31, 2sylbir 206 1  |-  ( ( A  e.  B  /\  A  e.  C )  ->  ( B  i^i  C
)  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726    =/= wne 2601    i^i cin 3321   (/)c0 3630
This theorem is referenced by:  minel  3685  disji  4202  disjiun  4204  onnseq  6608  uniinqs  6986  en3lplem1  7672  cplem1  7815  fpwwe2lem12  8518  limsupgre  12277  lmcls  17368  concn  17491  iunconlem  17492  concompclo  17500  2ndcsep  17524  txcls  17638  pthaus  17672  qtopeu  17750  trfbas2  17877  filss  17887  zfbas  17930  fmfnfm  17992  tsmsfbas  18159  restmetu  18619  qdensere  18806  reperflem  18851  reconnlem1  18859  metds0  18882  metnrmlem1a  18890  minveclem3b  19331  ovolicc2lem5  19419  taylfval  20277  disjif  24022  disjif2  24025  subfacp1lem6  24873  erdszelem5  24883  pconcon  24920  cvmseu  24965  lfinpfin  26385  locfincmp  26386  neibastop2lem  26391  sstotbnd3  26487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-in 3329  df-nul 3631
  Copyright terms: Public domain W3C validator