Theorem inelcm 4398

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ≠ wne 2943   ∩ cin 3886  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-v 3434  df-dif 3890  df-in 3894  df-nul 4257

This theorem is referenced by:  minel  4399  disji  5057  disjiun  5061  onnseq  8175  uniinqs  8586  en3lplem1  9370  cplem1  9647  fpwwe2lem11  10397  limsupgre  15190  cat1lem  17811  lmcls  22453  conncn  22577  iunconnlem  22578  conncompclo  22586  2ndcsep  22610  lfinpfin  22675  locfincmp  22677  txcls  22755  pthaus  22789  qtopeu  22867  trfbas2  22994  filss  23004  zfbas  23047  fmfnfm  23109  tsmsfbas  23279  restmetu  23726  qdensere  23933  reperflem  23981  reconnlem1  23989  metds0  24013  metnrmlem1a  24021  minveclem3b  24592  ovolicc2lem5  24685  taylfval  25518  wlk1walk  28006  wwlksm1edg  28246  disjif  30917  disjif2  30920  subfacp1lem6  33147  erdszelem5  33157  pconnconn  33193  cvmseu  33238  neibastop2lem  34549  topdifinffinlem  35518  sstotbnd3  35934  brtrclfv2  41335  corcltrcl  41347  disjinfi  42731