Theorem inelcm 4415

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ≠ wne 2930   ∩ cin 3898  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-v 3440  df-dif 3902  df-in 3906  df-nul 4284

This theorem is referenced by:  minel  4416  disji  5081  disjiun  5084  onnseq  8274  uniinqs  8732  en3lplem1  9519  cplem1  9799  fpwwe2lem11  10550  limsupgre  15402  cat1lem  18018  lmcls  23244  conncn  23368  iunconnlem  23369  conncompclo  23377  2ndcsep  23401  lfinpfin  23466  locfincmp  23468  txcls  23546  pthaus  23580  qtopeu  23658  trfbas2  23785  filss  23795  zfbas  23838  fmfnfm  23900  tsmsfbas  24070  restmetu  24512  qdensere  24711  reperflem  24761  reconnlem1  24769  metds0  24793  metnrmlem1a  24801  minveclem3b  25382  ovolicc2lem5  25476  taylfval  26320  wlk1walk  29661  wwlksm1edg  29903  disjif  32602  disjif2  32605  dfufd2lem  33579  subfacp1lem6  35328  erdszelem5  35338  pconnconn  35374  cvmseu  35419  neibastop2lem  36503  topdifinffinlem  37491  sstotbnd3  37916  brtrclfv2  43910  corcltrcl  43922  disjinfi  45378