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

Theorem inelcm 4173
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 3945 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
2 ne0i 4067 . 2 (𝐴 ∈ (𝐵𝐶) → (𝐵𝐶) ≠ ∅)
31, 2sylbir 225 1 ((𝐴𝐵𝐴𝐶) → (𝐵𝐶) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2144  wne 2942  cin 3720  c0 4061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-v 3351  df-dif 3724  df-in 3728  df-nul 4062
This theorem is referenced by:  minel  4174  disji  4769  disjiun  4772  onnseq  7593  uniinqs  7978  en3lplem1  8670  cplem1  8915  fpwwe2lem12  9664  limsupgre  14419  lmcls  21326  conncn  21449  iunconnlem  21450  conncompclo  21458  2ndcsep  21482  lfinpfin  21547  locfincmp  21549  txcls  21627  pthaus  21661  qtopeu  21739  trfbas2  21866  filss  21876  zfbas  21919  fmfnfm  21981  tsmsfbas  22150  restmetu  22594  qdensere  22792  reperflem  22840  reconnlem1  22848  metds0  22872  metnrmlem1a  22880  minveclem3b  23417  ovolicc2lem5  23508  taylfval  24332  wlk1walk  26769  wwlksm1edg  27014  disjif  29723  disjif2  29726  subfacp1lem6  31499  erdszelem5  31509  pconnconn  31545  cvmseu  31590  neibastop2lem  32686  topdifinffinlem  33525  sstotbnd3  33900  brtrclfv2  38538  corcltrcl  38550  disjinfi  39894
  Copyright terms: Public domain W3C validator