Theorem inelcm 4416

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925   ∩ cin 3902  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-in 3910  df-nul 4285

This theorem is referenced by:  minel  4417  disji  5077  disjiun  5080  onnseq  8267  uniinqs  8724  en3lplem1  9508  cplem1  9785  fpwwe2lem11  10535  limsupgre  15388  cat1lem  18003  lmcls  23187  conncn  23311  iunconnlem  23312  conncompclo  23320  2ndcsep  23344  lfinpfin  23409  locfincmp  23411  txcls  23489  pthaus  23523  qtopeu  23601  trfbas2  23728  filss  23738  zfbas  23781  fmfnfm  23843  tsmsfbas  24013  restmetu  24456  qdensere  24655  reperflem  24705  reconnlem1  24713  metds0  24737  metnrmlem1a  24745  minveclem3b  25326  ovolicc2lem5  25420  taylfval  26264  wlk1walk  29584  wwlksm1edg  29826  disjif  32522  disjif2  32525  dfufd2lem  33487  subfacp1lem6  35168  erdszelem5  35178  pconnconn  35214  cvmseu  35259  neibastop2lem  36344  topdifinffinlem  37331  sstotbnd3  37766  brtrclfv2  43710  corcltrcl  43722  disjinfi  45180