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

Theorem inelcm 3509
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 3358 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
2 ne0i 3461 . 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 1684    =/= wne 2446    i^i cin 3151   (/)c0 3455
This theorem is referenced by:  minel  3510  disji  4011  disjiun  4013  onnseq  6361  en3lplem1  7416  cplem1  7559  fpwwe2lem12  8263  limsupgre  11955  lmcls  17030  concn  17152  iunconlem  17153  concompclo  17161  2ndcsep  17185  txcls  17299  pthaus  17332  qtopeu  17407  trfbas2  17538  filss  17548  zfbas  17591  fmfnfm  17653  tsmsfbas  17810  qdensere  18279  reperflem  18323  reconnlem1  18331  metds0  18354  metnrmlem1a  18362  minveclem3b  18792  ovolicc2lem5  18880  taylfval  19738  disjif  23355  disjif2  23358  subfacp1lem6  23716  erdszelem5  23726  pconcon  23762  cvmseu  23807  uninqs  25039  lfinpfin  26303  locfincmp  26304  neibastop2lem  26309  sstotbnd3  26500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-in 3159  df-nul 3456
  Copyright terms: Public domain W3C validator