Theorem inelcm 4032

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990   ≠ wne 2794   ∩ cin 3573  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-in 3581  df-nul 3916

This theorem is referenced by:  minel  4033  minelOLD  4034  disji  4637  disjiun  4640  onnseq  7441  uniinqs  7827  en3lplem1  8511  cplem1  8752  fpwwe2lem12  9463  limsupgre  14212  lmcls  21106  conncn  21229  iunconnlem  21230  conncompclo  21238  2ndcsep  21262  lfinpfin  21327  locfincmp  21329  txcls  21407  pthaus  21441  qtopeu  21519  trfbas2  21647  filss  21657  zfbas  21700  fmfnfm  21762  tsmsfbas  21931  restmetu  22375  qdensere  22573  reperflem  22621  reconnlem1  22629  metds0  22653  metnrmlem1a  22661  minveclem3b  23199  ovolicc2lem5  23289  taylfval  24113  wlk1walk  26535  wwlksm1edg  26767  disjif  29391  disjif2  29394  subfacp1lem6  31167  erdszelem5  31177  pconnconn  31213  cvmseu  31258  neibastop2lem  32355  topdifinffinlem  33195  sstotbnd3  33575  brtrclfv2  38019  corcltrcl  38031  disjinfi  39380