Theorem inelcm 4410

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 4280	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
3	1, 2	sylbir 234	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105   ≠ wne 2940   ∩ cin 3896  ∅c0 4268

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-v 3443  df-dif 3900  df-in 3904  df-nul 4269

This theorem is referenced by:  minel  4411  disji  5072  disjiun  5076  onnseq  8237  uniinqs  8649  en3lplem1  9461  cplem1  9738  fpwwe2lem11  10490  limsupgre  15281  cat1lem  17900  lmcls  22551  conncn  22675  iunconnlem  22676  conncompclo  22684  2ndcsep  22708  lfinpfin  22773  locfincmp  22775  txcls  22853  pthaus  22887  qtopeu  22965  trfbas2  23092  filss  23102  zfbas  23145  fmfnfm  23207  tsmsfbas  23377  restmetu  23824  qdensere  24031  reperflem  24079  reconnlem1  24087  metds0  24111  metnrmlem1a  24119  minveclem3b  24690  ovolicc2lem5  24783  taylfval  25616  wlk1walk  28236  wwlksm1edg  28475  disjif  31145  disjif2  31148  subfacp1lem6  33387  erdszelem5  33397  pconnconn  33433  cvmseu  33478  neibastop2lem  34640  topdifinffinlem  35616  sstotbnd3  36032  brtrclfv2  41645  corcltrcl  41657  disjinfi  43047