Theorem inelcm 4421

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144   ≠ wne 2959   ∩ cin 3905  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-v 3458  df-dif 3909  df-in 3913  df-nul 4288

This theorem is referenced by:  minel  4422  disji  5087  disjiun  5090  onnseq  8317  uniinqs  8781  en3lplem1  9569  cplem1  9849  fpwwe2lem11  10601  limsupgre  15510  cat1lem  18131  lmcls  23364  conncn  23488  iunconnlem  23489  conncompclo  23497  2ndcsep  23521  lfinpfin  23586  locfincmp  23588  txcls  23666  pthaus  23700  qtopeu  23778  trfbas2  23905  filss  23915  zfbas  23958  fmfnfm  24020  tsmsfbas  24190  restmetu  24632  qdensere  24831  reperflem  24881  reconnlem1  24889  metds0  24913  metnrmlem1a  24921  minveclem3b  25492  ovolicc2lem5  25585  taylfval  26424  wlk1walk  29841  wwlksm1edg  30083  disjif  32780  disjif2  32783  dfufd2lem  33747  subfacp1lem6  35540  erdszelem5  35550  pconnconn  35586  cvmseu  35631  neibastop2lem  36725  topdifinffinlem  37846  sstotbnd3  38280  brtrclfv2  44308  corcltrcl  44320  disjinfi  45775