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

Theorem inelcm 4256
 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 4023 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4150 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 227 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2166   ≠ wne 2999   ∩ cin 3797  ∅c0 4144 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-v 3416  df-dif 3801  df-in 3805  df-nul 4145 This theorem is referenced by:  minel  4257  disji  4858  disjiun  4861  onnseq  7707  uniinqs  8092  en3lplem1  8784  cplem1  9029  fpwwe2lem12  9778  limsupgre  14589  lmcls  21477  conncn  21600  iunconnlem  21601  conncompclo  21609  2ndcsep  21633  lfinpfin  21698  locfincmp  21700  txcls  21778  pthaus  21812  qtopeu  21890  trfbas2  22017  filss  22027  zfbas  22070  fmfnfm  22132  tsmsfbas  22301  restmetu  22745  qdensere  22943  reperflem  22991  reconnlem1  22999  metds0  23023  metnrmlem1a  23031  minveclem3b  23596  ovolicc2lem5  23687  taylfval  24512  wlk1walk  26936  wwlksm1edg  27180  wwlksm1edgOLD  27181  disjif  29938  disjif2  29941  subfacp1lem6  31713  erdszelem5  31723  pconnconn  31759  cvmseu  31804  neibastop2lem  32893  topdifinffinlem  33740  sstotbnd3  34117  brtrclfv2  38860  corcltrcl  38872  disjinfi  40188
 Copyright terms: Public domain W3C validator