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

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