Theorem inelcm 4471

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106   ≠ wne 2938   ∩ cin 3962  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-v 3480  df-dif 3966  df-in 3970  df-nul 4340

This theorem is referenced by:  minel  4472  disji  5133  disjiun  5136  onnseq  8383  uniinqs  8836  en3lplem1  9650  cplem1  9927  fpwwe2lem11  10679  limsupgre  15514  cat1lem  18150  lmcls  23326  conncn  23450  iunconnlem  23451  conncompclo  23459  2ndcsep  23483  lfinpfin  23548  locfincmp  23550  txcls  23628  pthaus  23662  qtopeu  23740  trfbas2  23867  filss  23877  zfbas  23920  fmfnfm  23982  tsmsfbas  24152  restmetu  24599  qdensere  24806  reperflem  24854  reconnlem1  24862  metds0  24886  metnrmlem1a  24894  minveclem3b  25476  ovolicc2lem5  25570  taylfval  26415  wlk1walk  29672  wwlksm1edg  29911  disjif  32598  disjif2  32601  dfufd2lem  33557  subfacp1lem6  35170  erdszelem5  35180  pconnconn  35216  cvmseu  35261  neibastop2lem  36343  topdifinffinlem  37330  sstotbnd3  37763  brtrclfv2  43717  corcltrcl  43729  disjinfi  45135