Theorem inelcm 4406

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933   ∩ cin 3889  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275

This theorem is referenced by:  minel  4407  disji  5071  disjiun  5074  onnseq  8279  uniinqs  8739  en3lplem1  9528  cplem1  9808  fpwwe2lem11  10559  limsupgre  15438  cat1lem  18058  lmcls  23281  conncn  23405  iunconnlem  23406  conncompclo  23414  2ndcsep  23438  lfinpfin  23503  locfincmp  23505  txcls  23583  pthaus  23617  qtopeu  23695  trfbas2  23822  filss  23832  zfbas  23875  fmfnfm  23937  tsmsfbas  24107  restmetu  24549  qdensere  24748  reperflem  24798  reconnlem1  24806  metds0  24830  metnrmlem1a  24838  minveclem3b  25409  ovolicc2lem5  25502  taylfval  26339  wlk1walk  29726  wwlksm1edg  29968  disjif  32667  disjif2  32670  dfufd2lem  33628  subfacp1lem6  35387  erdszelem5  35397  pconnconn  35433  cvmseu  35478  neibastop2lem  36562  topdifinffinlem  37681  sstotbnd3  38115  brtrclfv2  44176  corcltrcl  44188  disjinfi  45644