Theorem inelcm 4396

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121   ≠ wne 2936   ∩ cin 3884  ∅c0 4264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-in 3892  df-nul 4265

This theorem is referenced by:  minel  4397  disji  5060  disjiun  5063  onnseq  8278  uniinqs  8738  en3lplem1  9528  cplem1  9808  fpwwe2lem11  10559  limsupgre  15438  cat1lem  18058  lmcls  23289  conncn  23413  iunconnlem  23414  conncompclo  23422  2ndcsep  23446  lfinpfin  23511  locfincmp  23513  txcls  23591  pthaus  23625  qtopeu  23703  trfbas2  23830  filss  23840  zfbas  23883  fmfnfm  23945  tsmsfbas  24115  restmetu  24557  qdensere  24756  reperflem  24806  reconnlem1  24814  metds0  24838  metnrmlem1a  24846  minveclem3b  25417  ovolicc2lem5  25510  taylfval  26346  wlk1walk  29729  wwlksm1edg  29971  disjif  32671  disjif2  32674  dfufd2lem  33644  subfacp1lem6  35428  erdszelem5  35438  pconnconn  35474  cvmseu  35519  neibastop2lem  36603  topdifinffinlem  37724  sstotbnd3  38158  brtrclfv2  44186  corcltrcl  44198  disjinfi  45653