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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ≠ wne 2956   ∩ cin 3898  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  minel  4419  disji  5088  disjiun  5091  onnseq  8352  uniinqs  8818  en3lplem1  9613  cplem1  9950  cplem1OLD  9951  fpwwe2lem11  10726  limsupgre  15648  cat1lem  18271  lmcls  23620  conncn  23744  iunconnlem  23745  conncompclo  23753  2ndcsep  23778  lfinpfin  23843  locfincmp  23845  txcls  23923  pthaus  23957  qtopeu  24035  trfbas2  24162  filss  24172  zfbas  24215  fmfnfm  24277  tsmsfbas  24447  restmetu  24889  qdensere  25088  reperflem  25138  reconnlem1  25146  metds0  25170  metnrmlem1a  25178  minveclem3b  25749  ovolicc2lem5  25842  taylfval  26686  prlnghpg  29424  wlk1walk  30219  wwlksm1edg  30470  disjif  33172  disjif2  33175  dfufd2lem  34081  subfacp1lem6  35950  erdszelem5  35960  pconnconn  35996  cvmseu  36041  neibastop2lem  37148  topdifinffinlem  38270  sstotbnd3  38710  brtrclfv2  44726  corcltrcl  44738  disjinfi  46206