Theorem inelcm 4440

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ≠ wne 2932   ∩ cin 3925  ∅c0 4308

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-in 3933  df-nul 4309

This theorem is referenced by:  minel  4441  disji  5104  disjiun  5107  onnseq  8358  uniinqs  8811  en3lplem1  9626  cplem1  9903  fpwwe2lem11  10655  limsupgre  15497  cat1lem  18109  lmcls  23240  conncn  23364  iunconnlem  23365  conncompclo  23373  2ndcsep  23397  lfinpfin  23462  locfincmp  23464  txcls  23542  pthaus  23576  qtopeu  23654  trfbas2  23781  filss  23791  zfbas  23834  fmfnfm  23896  tsmsfbas  24066  restmetu  24509  qdensere  24708  reperflem  24758  reconnlem1  24766  metds0  24790  metnrmlem1a  24798  minveclem3b  25380  ovolicc2lem5  25474  taylfval  26318  wlk1walk  29619  wwlksm1edg  29863  disjif  32559  disjif2  32562  dfufd2lem  33564  subfacp1lem6  35207  erdszelem5  35217  pconnconn  35253  cvmseu  35298  neibastop2lem  36378  topdifinffinlem  37365  sstotbnd3  37800  brtrclfv2  43751  corcltrcl  43763  disjinfi  45216