Theorem inelcm 4256

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2166   ≠ wne 2999   ∩ cin 3797  ∅c0 4144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-v 3416  df-dif 3801  df-in 3805  df-nul 4145

This theorem is referenced by:  minel  4257  disji  4858  disjiun  4861  onnseq  7707  uniinqs  8092  en3lplem1  8784  cplem1  9029  fpwwe2lem12  9778  limsupgre  14589  lmcls  21477  conncn  21600  iunconnlem  21601  conncompclo  21609  2ndcsep  21633  lfinpfin  21698  locfincmp  21700  txcls  21778  pthaus  21812  qtopeu  21890  trfbas2  22017  filss  22027  zfbas  22070  fmfnfm  22132  tsmsfbas  22301  restmetu  22745  qdensere  22943  reperflem  22991  reconnlem1  22999  metds0  23023  metnrmlem1a  23031  minveclem3b  23596  ovolicc2lem5  23687  taylfval  24512  wlk1walk  26936  wwlksm1edg  27180  wwlksm1edgOLD  27181  disjif  29938  disjif2  29941  subfacp1lem6  31713  erdszelem5  31723  pconnconn  31759  cvmseu  31804  neibastop2lem  32893  topdifinffinlem  33740  sstotbnd3  34117  brtrclfv2  38860  corcltrcl  38872  disjinfi  40188