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

Theorem inelcm 3847
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 3649 . 2  |-  ( A  e.  ( B  i^i  C )  <->  ( A  e.  B  /\  A  e.  C ) )
2 ne0i 3767 . 2  |-  ( A  e.  ( B  i^i  C )  ->  ( B  i^i  C )  =/=  (/) )
31, 2sylbir 216 1  |-  ( ( A  e.  B  /\  A  e.  C )  ->  ( B  i^i  C
)  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1868    =/= wne 2618    i^i cin 3435   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-v 3083  df-dif 3439  df-in 3443  df-nul 3762
This theorem is referenced by:  minel  3848  disji  4408  disjiun  4411  onnseq  7068  uniinqs  7448  en3lplem1  8122  cplem1  8362  fpwwe2lem12  9067  limsupgre  13530  limsupgreOLD  13531  lmcls  20305  concn  20428  iunconlem  20429  concompclo  20437  2ndcsep  20461  lfinpfin  20526  locfincmp  20528  txcls  20606  pthaus  20640  qtopeu  20718  trfbas2  20845  filss  20855  zfbas  20898  fmfnfm  20960  tsmsfbas  21129  restmetu  21572  qdensere  21777  reperflem  21823  reconnlem1  21831  metds0  21854  metnrmlem1a  21862  metds0OLD  21869  metnrmlem1aOLD  21877  minveclem3b  22357  minveclem3bOLD  22369  ovolicc2lem5  22462  taylfval  23301  wwlkm1edg  25449  disjif  28178  disjif2  28181  subfacp1lem6  29904  erdszelem5  29914  pconcon  29950  cvmseu  29995  neibastop2lem  31009  topdifinffinlem  31691  sstotbnd3  32022  brtrclfv2  36179  corcltrcl  36191  disjinfi  37318
  Copyright terms: Public domain W3C validator