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

Theorem inelcm 4410
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 4166 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4297 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 236 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wne 3013  cin 3932  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-v 3494  df-dif 3936  df-in 3940  df-nul 4289
This theorem is referenced by:  minel  4411  disji  5040  disjiun  5044  onnseq  7970  uniinqs  8366  en3lplem1  9063  cplem1  9306  fpwwe2lem12  10051  limsupgre  14826  lmcls  21838  conncn  21962  iunconnlem  21963  conncompclo  21971  2ndcsep  21995  lfinpfin  22060  locfincmp  22062  txcls  22140  pthaus  22174  qtopeu  22252  trfbas2  22379  filss  22389  zfbas  22432  fmfnfm  22494  tsmsfbas  22663  restmetu  23107  qdensere  23305  reperflem  23353  reconnlem1  23361  metds0  23385  metnrmlem1a  23393  minveclem3b  23958  ovolicc2lem5  24049  taylfval  24874  wlk1walk  27347  wwlksm1edg  27586  disjif  30256  disjif2  30259  subfacp1lem6  32329  erdszelem5  32339  pconnconn  32375  cvmseu  32420  neibastop2lem  33605  topdifinffinlem  34510  sstotbnd3  34935  brtrclfv2  39950  corcltrcl  39962  disjinfi  41330
  Copyright terms: Public domain W3C validator