Theorem inelcm 4425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2143   ≠ wne 2958   ∩ cin 3904  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3908  df-in 3912  df-nul 4287

This theorem is used by:  minel  4426  disji  5094  disjiun  5097  onnseq  8327  uniinqs  8791  en3lplem1  9577  cplem1  9875  cplem1OLD  9876  fpwwe2lem11  10630  limsupgre  15537  cat1lem  18157  lmcls  23468  conncn  23592  iunconnlem  23593  conncompclo  23601  2ndcsep  23625  lfinpfin  23690  locfincmp  23692  txcls  23770  pthaus  23804  qtopeu  23882  trfbas2  24009  filss  24019  zfbas  24062  fmfnfm  24124  tsmsfbas  24294  restmetu  24736  qdensere  24935  reperflem  24985  reconnlem1  24993  metds0  25017  metnrmlem1a  25025  minveclem3b  25596  ovolicc2lem5  25689  taylfval  26531  prlnghpg  29205  wlk1walk  29997  wwlksm1edg  30239  disjif  32932  disjif2  32935  dfufd2lem  33848  subfacp1lem6  35685  erdszelem5  35695  pconnconn  35731  cvmseu  35776  neibastop2lem  36899  topdifinffinlem  38021  sstotbnd3  38455  brtrclfv2  44481  corcltrcl  44493  disjinfi  45938