Theorem inelcm 4428

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 3930	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2		ne0i 4304	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
3	1, 2	sylbir 235	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925   ∩ cin 3913  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-in 3921  df-nul 4297

This theorem is referenced by:  minel  4429  disji  5092  disjiun  5095  onnseq  8313  uniinqs  8770  en3lplem1  9565  cplem1  9842  fpwwe2lem11  10594  limsupgre  15447  cat1lem  18058  lmcls  23189  conncn  23313  iunconnlem  23314  conncompclo  23322  2ndcsep  23346  lfinpfin  23411  locfincmp  23413  txcls  23491  pthaus  23525  qtopeu  23603  trfbas2  23730  filss  23740  zfbas  23783  fmfnfm  23845  tsmsfbas  24015  restmetu  24458  qdensere  24657  reperflem  24707  reconnlem1  24715  metds0  24739  metnrmlem1a  24747  minveclem3b  25328  ovolicc2lem5  25422  taylfval  26266  wlk1walk  29567  wwlksm1edg  29811  disjif  32507  disjif2  32510  dfufd2lem  33520  subfacp1lem6  35172  erdszelem5  35182  pconnconn  35218  cvmseu  35263  neibastop2lem  36348  topdifinffinlem  37335  sstotbnd3  37770  brtrclfv2  43716  corcltrcl  43728  disjinfi  45186