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

Theorem inelcm 4009
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 3779 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 3902 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 225 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  wne 2790  cin 3558  c0 3896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3191  df-dif 3562  df-in 3566  df-nul 3897
This theorem is referenced by:  minel  4010  minelOLD  4011  disji  4605  disjiun  4608  onnseq  7393  uniinqs  7779  en3lplem1  8463  cplem1  8704  fpwwe2lem12  9415  limsupgre  14154  lmcls  21029  conncn  21152  iunconnlem  21153  conncompclo  21161  2ndcsep  21185  lfinpfin  21250  locfincmp  21252  txcls  21330  pthaus  21364  qtopeu  21442  trfbas2  21570  filss  21580  zfbas  21623  fmfnfm  21685  tsmsfbas  21854  restmetu  22298  qdensere  22496  reperflem  22544  reconnlem1  22552  metds0  22576  metnrmlem1a  22584  minveclem3b  23122  ovolicc2lem5  23212  taylfval  24034  wlk1walk  26421  wwlksm1edg  26653  disjif  29259  disjif2  29262  subfacp1lem6  30910  erdszelem5  30920  pconnconn  30956  cvmseu  31001  neibastop2lem  32032  topdifinffinlem  32862  sstotbnd3  33242  brtrclfv2  37535  corcltrcl  37547  disjinfi  38885
  Copyright terms: Public domain W3C validator