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

Theorem inelcm 4397
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 3935 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4283 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 238 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  wne 3014  cin 3918  c0 4276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3015  df-v 3482  df-dif 3922  df-in 3926  df-nul 4277
This theorem is referenced by:  minel  4398  disji  5035  disjiun  5039  onnseq  7977  uniinqs  8373  en3lplem1  9072  cplem1  9315  fpwwe2lem12  10061  limsupgre  14838  lmcls  21910  conncn  22034  iunconnlem  22035  conncompclo  22043  2ndcsep  22067  lfinpfin  22132  locfincmp  22134  txcls  22212  pthaus  22246  qtopeu  22324  trfbas2  22451  filss  22461  zfbas  22504  fmfnfm  22566  tsmsfbas  22736  restmetu  23180  qdensere  23378  reperflem  23426  reconnlem1  23434  metds0  23458  metnrmlem1a  23466  minveclem3b  24035  ovolicc2lem5  24128  taylfval  24957  wlk1walk  27431  wwlksm1edg  27670  disjif  30339  disjif2  30342  subfacp1lem6  32489  erdszelem5  32499  pconnconn  32535  cvmseu  32580  neibastop2lem  33765  topdifinffinlem  34709  sstotbnd3  35159  brtrclfv2  40344  corcltrcl  40356  disjinfi  41745
  Copyright terms: Public domain W3C validator