Theorem inelcm 4425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ≠ wne 2960   ∩ cin 3905  ∅c0 4286

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-in 3913  df-nul 4287

This theorem is used by:  minel  4426  disji  5096  disjiun  5099  onnseq  8337  uniinqs  8801  en3lplem1  9588  cplem1  9886  cplem1OLD  9887  fpwwe2lem11  10645  limsupgre  15560  cat1lem  18179  lmcls  23513  conncn  23637  iunconnlem  23638  conncompclo  23646  2ndcsep  23671  lfinpfin  23736  locfincmp  23738  txcls  23816  pthaus  23850  qtopeu  23928  trfbas2  24055  filss  24065  zfbas  24108  fmfnfm  24170  tsmsfbas  24340  restmetu  24782  qdensere  24981  reperflem  25031  reconnlem1  25039  metds0  25063  metnrmlem1a  25071  minveclem3b  25642  ovolicc2lem5  25735  taylfval  26577  prlnghpg  29255  wlk1walk  30050  wwlksm1edg  30301  disjif  32998  disjif2  33001  dfufd2lem  33907  subfacp1lem6  35718  erdszelem5  35728  pconnconn  35764  cvmseu  35809  neibastop2lem  36932  topdifinffinlem  38054  sstotbnd3  38489  brtrclfv2  44530  corcltrcl  44542  disjinfi  45987