Theorem inelcm 4469

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099   ≠ wne 2930   ∩ cin 3946  ∅c0 4325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-v 3464  df-dif 3950  df-in 3954  df-nul 4326

This theorem is referenced by:  minel  4470  disji  5136  disjiun  5140  onnseq  8374  uniinqs  8826  en3lplem1  9655  cplem1  9932  fpwwe2lem11  10684  limsupgre  15483  cat1lem  18118  lmcls  23297  conncn  23421  iunconnlem  23422  conncompclo  23430  2ndcsep  23454  lfinpfin  23519  locfincmp  23521  txcls  23599  pthaus  23633  qtopeu  23711  trfbas2  23838  filss  23848  zfbas  23891  fmfnfm  23953  tsmsfbas  24123  restmetu  24570  qdensere  24777  reperflem  24825  reconnlem1  24833  metds0  24857  metnrmlem1a  24865  minveclem3b  25447  ovolicc2lem5  25541  taylfval  26386  wlk1walk  29576  wwlksm1edg  29815  disjif  32498  disjif2  32501  dfufd2lem  33424  subfacp1lem6  35013  erdszelem5  35023  pconnconn  35059  cvmseu  35104  neibastop2lem  36072  topdifinffinlem  37054  sstotbnd3  37477  brtrclfv2  43394  corcltrcl  43406  disjinfi  44799