Theorem inelcm 4418

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ≠ wne 2955   ∩ cin 3898  ∅c0 4279

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  minel  4419  disji  5088  disjiun  5091  onnseq  8334  uniinqs  8800  en3lplem1  9594  cplem1  9892  cplem1OLD  9893  fpwwe2lem11  10653  limsupgre  15571  cat1lem  18188  lmcls  23530  conncn  23654  iunconnlem  23655  conncompclo  23663  2ndcsep  23688  lfinpfin  23753  locfincmp  23755  txcls  23833  pthaus  23867  qtopeu  23945  trfbas2  24072  filss  24082  zfbas  24125  fmfnfm  24187  tsmsfbas  24357  restmetu  24799  qdensere  24998  reperflem  25048  reconnlem1  25056  metds0  25080  metnrmlem1a  25088  minveclem3b  25659  ovolicc2lem5  25752  taylfval  26598  prlnghpg  29306  wlk1walk  30101  wwlksm1edg  30352  disjif  33054  disjif2  33057  dfufd2lem  33962  subfacp1lem6  35767  erdszelem5  35777  pconnconn  35813  cvmseu  35858  neibastop2lem  36982  topdifinffinlem  38104  sstotbnd3  38529  brtrclfv2  44570  corcltrcl  44582  disjinfi  46027