Theorem inelcm 4419

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

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

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 3444  df-dif 3906  df-in 3910  df-nul 4288

This theorem is referenced by:  minel  4420  disji  5085  disjiun  5088  onnseq  8288  uniinqs  8748  en3lplem1  9535  cplem1  9815  fpwwe2lem11  10566  limsupgre  15418  cat1lem  18034  lmcls  23263  conncn  23387  iunconnlem  23388  conncompclo  23396  2ndcsep  23420  lfinpfin  23485  locfincmp  23487  txcls  23565  pthaus  23599  qtopeu  23677  trfbas2  23804  filss  23814  zfbas  23857  fmfnfm  23919  tsmsfbas  24089  restmetu  24531  qdensere  24730  reperflem  24780  reconnlem1  24788  metds0  24812  metnrmlem1a  24820  minveclem3b  25401  ovolicc2lem5  25495  taylfval  26339  wlk1walk  29730  wwlksm1edg  29972  disjif  32671  disjif2  32674  dfufd2lem  33648  subfacp1lem6  35407  erdszelem5  35417  pconnconn  35453  cvmseu  35498  neibastop2lem  36582  topdifinffinlem  37629  sstotbnd3  38056  brtrclfv2  44112  corcltrcl  44124  disjinfi  45580