Theorem inelcm 4258

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164   ≠ wne 2999   ∩ cin 3797  ∅c0 4146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-v 3416  df-dif 3801  df-in 3805  df-nul 4147

This theorem is referenced by:  minel  4259  disji  4860  disjiun  4863  onnseq  7712  uniinqs  8097  en3lplem1  8791  cplem1  9036  fpwwe2lem12  9785  limsupgre  14596  lmcls  21484  conncn  21607  iunconnlem  21608  conncompclo  21616  2ndcsep  21640  lfinpfin  21705  locfincmp  21707  txcls  21785  pthaus  21819  qtopeu  21897  trfbas2  22024  filss  22034  zfbas  22077  fmfnfm  22139  tsmsfbas  22308  restmetu  22752  qdensere  22950  reperflem  22998  reconnlem1  23006  metds0  23030  metnrmlem1a  23038  minveclem3b  23603  ovolicc2lem5  23694  taylfval  24519  wlk1walk  26943  wwlksm1edg  27187  wwlksm1edgOLD  27188  disjif  29934  disjif2  29937  subfacp1lem6  31709  erdszelem5  31719  pconnconn  31755  cvmseu  31800  neibastop2lem  32888  topdifinffinlem  33739  sstotbnd3  34116  brtrclfv2  38859  corcltrcl  38871  disjinfi  40187