Theorem inelcm 4488

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ≠ wne 2946   ∩ cin 3975  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-in 3983  df-nul 4353

This theorem is referenced by:  minel  4489  disji  5151  disjiun  5154  onnseq  8400  uniinqs  8855  en3lplem1  9681  cplem1  9958  fpwwe2lem11  10710  limsupgre  15527  cat1lem  18163  lmcls  23331  conncn  23455  iunconnlem  23456  conncompclo  23464  2ndcsep  23488  lfinpfin  23553  locfincmp  23555  txcls  23633  pthaus  23667  qtopeu  23745  trfbas2  23872  filss  23882  zfbas  23925  fmfnfm  23987  tsmsfbas  24157  restmetu  24604  qdensere  24811  reperflem  24859  reconnlem1  24867  metds0  24891  metnrmlem1a  24899  minveclem3b  25481  ovolicc2lem5  25575  taylfval  26418  wlk1walk  29675  wwlksm1edg  29914  disjif  32600  disjif2  32603  dfufd2lem  33542  subfacp1lem6  35153  erdszelem5  35163  pconnconn  35199  cvmseu  35244  neibastop2lem  36326  topdifinffinlem  37313  sstotbnd3  37736  brtrclfv2  43689  corcltrcl  43701  disjinfi  45099