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

Theorem inelcm 3984
Description: The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
Assertion
Ref Expression
inelcm ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)

Proof of Theorem inelcm
StepHypRef Expression
1 elin 3758 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 3880 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 224 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wne 2780  cin 3539  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-in 3547  df-nul 3875
This theorem is referenced by:  minel  3985  minelOLD  3986  disji  4570  disjiun  4573  onnseq  7328  uniinqs  7714  en3lplem1  8394  cplem1  8635  fpwwe2lem12  9342  limsupgre  14060  lmcls  20916  concn  21039  iunconlem  21040  concompclo  21048  2ndcsep  21072  lfinpfin  21137  locfincmp  21139  txcls  21217  pthaus  21251  qtopeu  21329  trfbas2  21457  filss  21467  zfbas  21510  fmfnfm  21572  tsmsfbas  21741  restmetu  22185  qdensere  22383  reperflem  22429  reconnlem1  22437  metds0  22461  metnrmlem1a  22469  minveclem3b  23007  ovolicc2lem5  23096  taylfval  23917  wwlkm1edg  26263  disjif  28773  disjif2  28776  subfacp1lem6  30421  erdszelem5  30431  pconcon  30467  cvmseu  30512  neibastop2lem  31525  topdifinffinlem  32371  sstotbnd3  32745  brtrclfv2  37038  corcltrcl  37050  disjinfi  38375  1wlk1walk  40843  wwlksm1edg  41078
  Copyright terms: Public domain W3C validator