Theorem inelcm 4414

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   ≠ wne 3016   ∩ cin 3935  ∅c0 4291

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3496  df-dif 3939  df-in 3943  df-nul 4292

This theorem is referenced by:  minel  4415  disji  5049  disjiun  5053  onnseq  7981  uniinqs  8377  en3lplem1  9075  cplem1  9318  fpwwe2lem12  10063  limsupgre  14838  lmcls  21910  conncn  22034  iunconnlem  22035  conncompclo  22043  2ndcsep  22067  lfinpfin  22132  locfincmp  22134  txcls  22212  pthaus  22246  qtopeu  22324  trfbas2  22451  filss  22461  zfbas  22504  fmfnfm  22566  tsmsfbas  22736  restmetu  23180  qdensere  23378  reperflem  23426  reconnlem1  23434  metds0  23458  metnrmlem1a  23466  minveclem3b  24031  ovolicc2lem5  24122  taylfval  24947  wlk1walk  27420  wwlksm1edg  27659  disjif  30328  disjif2  30331  subfacp1lem6  32432  erdszelem5  32442  pconnconn  32478  cvmseu  32523  neibastop2lem  33708  topdifinffinlem  34631  sstotbnd3  35069  brtrclfv2  40092  corcltrcl  40104  disjinfi  41474