Theorem inelcm 4395

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121   ≠ wne 2936   ∩ cin 3883  ∅c0 4263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3887  df-in 3891  df-nul 4264

This theorem is referenced by:  minel  4396  disji  5059  disjiun  5062  onnseq  8277  uniinqs  8738  en3lplem1  9528  cplem1  9808  fpwwe2lem11  10560  limsupgre  15438  cat1lem  18058  lmcls  23288  conncn  23412  iunconnlem  23413  conncompclo  23421  2ndcsep  23445  lfinpfin  23510  locfincmp  23512  txcls  23590  pthaus  23624  qtopeu  23702  trfbas2  23829  filss  23839  zfbas  23882  fmfnfm  23944  tsmsfbas  24114  restmetu  24556  qdensere  24755  reperflem  24805  reconnlem1  24813  metds0  24837  metnrmlem1a  24845  minveclem3b  25416  ovolicc2lem5  25509  taylfval  26345  wlk1walk  29727  wwlksm1edg  29969  disjif  32669  disjif2  32672  dfufd2lem  33642  subfacp1lem6  35426  erdszelem5  35436  pconnconn  35472  cvmseu  35517  neibastop2lem  36601  topdifinffinlem  37722  sstotbnd3  38156  brtrclfv2  44184  corcltrcl  44196  disjinfi  45651