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

Theorem inelcm 4469
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 3963 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4337 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 234 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2099  wne 2930  cin 3946  c0 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-v 3464  df-dif 3950  df-in 3954  df-nul 4326
This theorem is referenced by:  minel  4470  disji  5136  disjiun  5140  onnseq  8374  uniinqs  8826  en3lplem1  9655  cplem1  9932  fpwwe2lem11  10684  limsupgre  15483  cat1lem  18118  lmcls  23297  conncn  23421  iunconnlem  23422  conncompclo  23430  2ndcsep  23454  lfinpfin  23519  locfincmp  23521  txcls  23599  pthaus  23633  qtopeu  23711  trfbas2  23838  filss  23848  zfbas  23891  fmfnfm  23953  tsmsfbas  24123  restmetu  24570  qdensere  24777  reperflem  24825  reconnlem1  24833  metds0  24857  metnrmlem1a  24865  minveclem3b  25447  ovolicc2lem5  25541  taylfval  26386  wlk1walk  29576  wwlksm1edg  29815  disjif  32498  disjif2  32501  dfufd2lem  33424  subfacp1lem6  35013  erdszelem5  35023  pconnconn  35059  cvmseu  35104  neibastop2lem  36072  topdifinffinlem  37054  sstotbnd3  37477  brtrclfv2  43394  corcltrcl  43406  disjinfi  44799
  Copyright terms: Public domain W3C validator