Theorem inelcm 4431

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   ≠ wne 2964   ∩ cin 3912  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3465  df-dif 3916  df-in 3920  df-nul 4295

This theorem is referenced by:  minel  4432  disji  5098  disjiun  5101  onnseq  8331  uniinqs  8795  en3lplem1  9581  cplem1  9875  fpwwe2lem11  10626  limsupgre  15532  cat1lem  18153  lmcls  23428  conncn  23552  iunconnlem  23553  conncompclo  23561  2ndcsep  23585  lfinpfin  23650  locfincmp  23652  txcls  23730  pthaus  23764  qtopeu  23842  trfbas2  23969  filss  23979  zfbas  24022  fmfnfm  24084  tsmsfbas  24254  restmetu  24696  qdensere  24895  reperflem  24945  reconnlem1  24953  metds0  24977  metnrmlem1a  24985  minveclem3b  25556  ovolicc2lem5  25649  taylfval  26488  prlnghpg  29151  wlk1walk  29929  wwlksm1edg  30171  disjif  32864  disjif2  32867  dfufd2lem  33784  subfacp1lem6  35610  erdszelem5  35620  pconnconn  35656  cvmseu  35701  neibastop2lem  36794  topdifinffinlem  37915  sstotbnd3  38349  brtrclfv2  44379  corcltrcl  44391  disjinfi  45836