Theorem inelcm 4412

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ≠ wne 2928   ∩ cin 3896  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-in 3904  df-nul 4281

This theorem is referenced by:  minel  4413  disji  5074  disjiun  5077  onnseq  8264  uniinqs  8721  en3lplem1  9502  cplem1  9782  fpwwe2lem11  10532  limsupgre  15388  cat1lem  18003  lmcls  23217  conncn  23341  iunconnlem  23342  conncompclo  23350  2ndcsep  23374  lfinpfin  23439  locfincmp  23441  txcls  23519  pthaus  23553  qtopeu  23631  trfbas2  23758  filss  23768  zfbas  23811  fmfnfm  23873  tsmsfbas  24043  restmetu  24485  qdensere  24684  reperflem  24734  reconnlem1  24742  metds0  24766  metnrmlem1a  24774  minveclem3b  25355  ovolicc2lem5  25449  taylfval  26293  wlk1walk  29617  wwlksm1edg  29859  disjif  32558  disjif2  32561  dfufd2lem  33514  subfacp1lem6  35229  erdszelem5  35239  pconnconn  35275  cvmseu  35320  neibastop2lem  36404  topdifinffinlem  37391  sstotbnd3  37815  brtrclfv2  43819  corcltrcl  43831  disjinfi  45288