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

Theorem inelcm 4429
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 3931 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4299 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 234 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wne 2944  cin 3914  c0 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-v 3450  df-dif 3918  df-in 3922  df-nul 4288
This theorem is referenced by:  minel  4430  disji  5093  disjiun  5097  onnseq  8295  uniinqs  8743  en3lplem1  9555  cplem1  9832  fpwwe2lem11  10584  limsupgre  15370  cat1lem  17989  lmcls  22669  conncn  22793  iunconnlem  22794  conncompclo  22802  2ndcsep  22826  lfinpfin  22891  locfincmp  22893  txcls  22971  pthaus  23005  qtopeu  23083  trfbas2  23210  filss  23220  zfbas  23263  fmfnfm  23325  tsmsfbas  23495  restmetu  23942  qdensere  24149  reperflem  24197  reconnlem1  24205  metds0  24229  metnrmlem1a  24237  minveclem3b  24808  ovolicc2lem5  24901  taylfval  25734  wlk1walk  28629  wwlksm1edg  28868  disjif  31538  disjif2  31541  subfacp1lem6  33819  erdszelem5  33829  pconnconn  33865  cvmseu  33910  neibastop2lem  34861  topdifinffinlem  35847  sstotbnd3  36264  brtrclfv2  42073  corcltrcl  42085  disjinfi  43486
  Copyright terms: Public domain W3C validator