Theorem inelcm 4465

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ≠ wne 2940   ∩ cin 3950  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334

This theorem is referenced by:  minel  4466  disji  5128  disjiun  5131  onnseq  8384  uniinqs  8837  en3lplem1  9652  cplem1  9929  fpwwe2lem11  10681  limsupgre  15517  cat1lem  18141  lmcls  23310  conncn  23434  iunconnlem  23435  conncompclo  23443  2ndcsep  23467  lfinpfin  23532  locfincmp  23534  txcls  23612  pthaus  23646  qtopeu  23724  trfbas2  23851  filss  23861  zfbas  23904  fmfnfm  23966  tsmsfbas  24136  restmetu  24583  qdensere  24790  reperflem  24840  reconnlem1  24848  metds0  24872  metnrmlem1a  24880  minveclem3b  25462  ovolicc2lem5  25556  taylfval  26400  wlk1walk  29657  wwlksm1edg  29901  disjif  32591  disjif2  32594  dfufd2lem  33577  subfacp1lem6  35190  erdszelem5  35200  pconnconn  35236  cvmseu  35281  neibastop2lem  36361  topdifinffinlem  37348  sstotbnd3  37783  brtrclfv2  43740  corcltrcl  43752  disjinfi  45197