MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inelcm Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 elin 3967 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4341 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 235 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator