Theorem inelcm 4395

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ≠ wne 2942   ∩ cin 3882  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-v 3424  df-dif 3886  df-in 3890  df-nul 4254

This theorem is referenced by:  minel  4396  disji  5053  disjiun  5057  onnseq  8146  uniinqs  8544  en3lplem1  9300  cplem1  9578  fpwwe2lem11  10328  limsupgre  15118  cat1lem  17727  lmcls  22361  conncn  22485  iunconnlem  22486  conncompclo  22494  2ndcsep  22518  lfinpfin  22583  locfincmp  22585  txcls  22663  pthaus  22697  qtopeu  22775  trfbas2  22902  filss  22912  zfbas  22955  fmfnfm  23017  tsmsfbas  23187  restmetu  23632  qdensere  23839  reperflem  23887  reconnlem1  23895  metds0  23919  metnrmlem1a  23927  minveclem3b  24497  ovolicc2lem5  24590  taylfval  25423  wlk1walk  27908  wwlksm1edg  28147  disjif  30818  disjif2  30821  subfacp1lem6  33047  erdszelem5  33057  pconnconn  33093  cvmseu  33138  neibastop2lem  34476  topdifinffinlem  35445  sstotbnd3  35861  brtrclfv2  41224  corcltrcl  41236  disjinfi  42620