Theorem inelcm 4424

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

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

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 3446  df-dif 3914  df-in 3918  df-nul 4293

This theorem is referenced by:  minel  4425  disji  5087  disjiun  5090  onnseq  8290  uniinqs  8747  en3lplem1  9541  cplem1  9818  fpwwe2lem11  10570  limsupgre  15423  cat1lem  18038  lmcls  23222  conncn  23346  iunconnlem  23347  conncompclo  23355  2ndcsep  23379  lfinpfin  23444  locfincmp  23446  txcls  23524  pthaus  23558  qtopeu  23636  trfbas2  23763  filss  23773  zfbas  23816  fmfnfm  23878  tsmsfbas  24048  restmetu  24491  qdensere  24690  reperflem  24740  reconnlem1  24748  metds0  24772  metnrmlem1a  24780  minveclem3b  25361  ovolicc2lem5  25455  taylfval  26299  wlk1walk  29619  wwlksm1edg  29861  disjif  32557  disjif2  32560  dfufd2lem  33513  subfacp1lem6  35165  erdszelem5  35175  pconnconn  35211  cvmseu  35256  neibastop2lem  36341  topdifinffinlem  37328  sstotbnd3  37763  brtrclfv2  43709  corcltrcl  43721  disjinfi  45179