Theorem inelcm 4418

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933   ∩ cin 3901  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3443  df-dif 3905  df-in 3909  df-nul 4287

This theorem is referenced by:  minel  4419  disji  5084  disjiun  5087  onnseq  8278  uniinqs  8738  en3lplem1  9525  cplem1  9805  fpwwe2lem11  10556  limsupgre  15408  cat1lem  18024  lmcls  23250  conncn  23374  iunconnlem  23375  conncompclo  23383  2ndcsep  23407  lfinpfin  23472  locfincmp  23474  txcls  23552  pthaus  23586  qtopeu  23664  trfbas2  23791  filss  23801  zfbas  23844  fmfnfm  23906  tsmsfbas  24076  restmetu  24518  qdensere  24717  reperflem  24767  reconnlem1  24775  metds0  24799  metnrmlem1a  24807  minveclem3b  25388  ovolicc2lem5  25482  taylfval  26326  wlk1walk  29716  wwlksm1edg  29958  disjif  32656  disjif2  32659  dfufd2lem  33632  subfacp1lem6  35381  erdszelem5  35391  pconnconn  35427  cvmseu  35472  neibastop2lem  36556  topdifinffinlem  37554  sstotbnd3  37979  brtrclfv2  44035  corcltrcl  44047  disjinfi  45503