Theorem inelcm 4465

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ≠ wne 2941   ∩ cin 3948  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-in 3956  df-nul 4324

This theorem is referenced by:  minel  4466  disji  5132  disjiun  5136  onnseq  8344  uniinqs  8791  en3lplem1  9607  cplem1  9884  fpwwe2lem11  10636  limsupgre  15425  cat1lem  18046  lmcls  22806  conncn  22930  iunconnlem  22931  conncompclo  22939  2ndcsep  22963  lfinpfin  23028  locfincmp  23030  txcls  23108  pthaus  23142  qtopeu  23220  trfbas2  23347  filss  23357  zfbas  23400  fmfnfm  23462  tsmsfbas  23632  restmetu  24079  qdensere  24286  reperflem  24334  reconnlem1  24342  metds0  24366  metnrmlem1a  24374  minveclem3b  24945  ovolicc2lem5  25038  taylfval  25871  wlk1walk  28927  wwlksm1edg  29166  disjif  31840  disjif2  31843  subfacp1lem6  34207  erdszelem5  34217  pconnconn  34253  cvmseu  34298  neibastop2lem  35293  topdifinffinlem  36276  sstotbnd3  36692  brtrclfv2  42526  corcltrcl  42538  disjinfi  43939