Theorem inelcm 4431

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ≠ wne 2926   ∩ cin 3916  ∅c0 4299

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-in 3924  df-nul 4300

This theorem is referenced by:  minel  4432  disji  5095  disjiun  5098  onnseq  8316  uniinqs  8773  en3lplem1  9572  cplem1  9849  fpwwe2lem11  10601  limsupgre  15454  cat1lem  18065  lmcls  23196  conncn  23320  iunconnlem  23321  conncompclo  23329  2ndcsep  23353  lfinpfin  23418  locfincmp  23420  txcls  23498  pthaus  23532  qtopeu  23610  trfbas2  23737  filss  23747  zfbas  23790  fmfnfm  23852  tsmsfbas  24022  restmetu  24465  qdensere  24664  reperflem  24714  reconnlem1  24722  metds0  24746  metnrmlem1a  24754  minveclem3b  25335  ovolicc2lem5  25429  taylfval  26273  wlk1walk  29574  wwlksm1edg  29818  disjif  32514  disjif2  32517  dfufd2lem  33527  subfacp1lem6  35179  erdszelem5  35189  pconnconn  35225  cvmseu  35270  neibastop2lem  36355  topdifinffinlem  37342  sstotbnd3  37777  brtrclfv2  43723  corcltrcl  43735  disjinfi  45193