Theorem inelcm 4405

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2932   ∩ cin 3888  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-in 3896  df-nul 4274

This theorem is referenced by:  minel  4406  disji  5070  disjiun  5073  onnseq  8284  uniinqs  8744  en3lplem1  9533  cplem1  9813  fpwwe2lem11  10564  limsupgre  15443  cat1lem  18063  lmcls  23267  conncn  23391  iunconnlem  23392  conncompclo  23400  2ndcsep  23424  lfinpfin  23489  locfincmp  23491  txcls  23569  pthaus  23603  qtopeu  23681  trfbas2  23808  filss  23818  zfbas  23861  fmfnfm  23923  tsmsfbas  24093  restmetu  24535  qdensere  24734  reperflem  24784  reconnlem1  24792  metds0  24816  metnrmlem1a  24824  minveclem3b  25395  ovolicc2lem5  25488  taylfval  26324  wlk1walk  29707  wwlksm1edg  29949  disjif  32648  disjif2  32651  dfufd2lem  33609  subfacp1lem6  35367  erdszelem5  35377  pconnconn  35413  cvmseu  35458  neibastop2lem  36542  topdifinffinlem  37663  sstotbnd3  38097  brtrclfv2  44154  corcltrcl  44166  disjinfi  45622