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

Theorem inelcm 3867
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 3672 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
2 ne0i 3776 . 2  |-  ( A  e.  ( B  i^i  C )  ->  ( B  i^i  C )  =/=  (/) )
31, 2sylbir 213 1  |-  ( ( A  e.  B  /\  A  e.  C )  ->  ( B  i^i  C
)  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804    =/= wne 2638    i^i cin 3460   (/)c0 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-in 3468  df-nul 3771
This theorem is referenced by:  minel  3868  disji  4425  disjiun  4427  onnseq  7017  uniinqs  7393  en3lplem1  8034  cplem1  8310  fpwwe2lem12  9022  swrdn0  12637  limsupgre  13286  lmcls  19781  concn  19905  iunconlem  19906  concompclo  19914  2ndcsep  19938  lfinpfin  20003  locfincmp  20005  txcls  20083  pthaus  20117  qtopeu  20195  trfbas2  20322  filss  20332  zfbas  20375  fmfnfm  20437  tsmsfbas  20604  restmetu  21068  qdensere  21255  reperflem  21301  reconnlem1  21309  metds0  21332  metnrmlem1a  21340  minveclem3b  21821  ovolicc2lem5  21910  taylfval  22732  wwlkm1edg  24713  disjif  27417  disjif2  27420  subfacp1lem6  28607  erdszelem5  28617  pconcon  28654  cvmseu  28699  neibastop2lem  30154  sstotbnd3  30248
  Copyright terms: Public domain W3C validator