Theorem inelcm 4463

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

Step	Hyp	Ref	Expression
1		elin 3963	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2		ne0i 4333	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
3	1, 2	sylbir 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ≠ wne 2940   ∩ cin 3946  ∅c0 4321

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3950  df-in 3954  df-nul 4322

This theorem is referenced by:  minel  4464  disji  5130  disjiun  5134  onnseq  8340  uniinqs  8787  en3lplem1  9603  cplem1  9880  fpwwe2lem11  10632  limsupgre  15421  cat1lem  18042  lmcls  22797  conncn  22921  iunconnlem  22922  conncompclo  22930  2ndcsep  22954  lfinpfin  23019  locfincmp  23021  txcls  23099  pthaus  23133  qtopeu  23211  trfbas2  23338  filss  23348  zfbas  23391  fmfnfm  23453  tsmsfbas  23623  restmetu  24070  qdensere  24277  reperflem  24325  reconnlem1  24333  metds0  24357  metnrmlem1a  24365  minveclem3b  24936  ovolicc2lem5  25029  taylfval  25862  wlk1walk  28885  wwlksm1edg  29124  disjif  31796  disjif2  31799  subfacp1lem6  34164  erdszelem5  34174  pconnconn  34210  cvmseu  34255  neibastop2lem  35233  topdifinffinlem  36216  sstotbnd3  36632  brtrclfv2  42463  corcltrcl  42475  disjinfi  43876