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

Theorem inelcm 3733
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 3539 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
2 ne0i 3643 . 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 1756    =/= wne 2606    i^i cin 3327   (/)c0 3637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-v 2974  df-dif 3331  df-in 3335  df-nul 3638
This theorem is referenced by:  minel  3734  disji  4280  disjiun  4282  onnseq  6805  uniinqs  7180  en3lplem1  7820  cplem1  8096  fpwwe2lem12  8808  swrdn0  12324  limsupgre  12959  lmcls  18906  concn  19030  iunconlem  19031  concompclo  19039  2ndcsep  19063  txcls  19177  pthaus  19211  qtopeu  19289  trfbas2  19416  filss  19426  zfbas  19469  fmfnfm  19531  tsmsfbas  19698  restmetu  20162  qdensere  20349  reperflem  20395  reconnlem1  20403  metds0  20426  metnrmlem1a  20434  minveclem3b  20915  ovolicc2lem5  21004  taylfval  21824  disjif  25922  disjif2  25925  subfacp1lem6  27073  erdszelem5  27083  pconcon  27120  cvmseu  27165  lfinpfin  28575  locfincmp  28576  neibastop2lem  28581  sstotbnd3  28675  wwlkm1edg  30367
  Copyright terms: Public domain W3C validator