Theorem sstr 3987

Description: Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)

Assertion

Ref	Expression
sstr	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Proof of Theorem sstr

Step	Hyp	Ref	Expression
1		sstr2 3986	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3945

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 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962

This theorem is referenced by:  sstrd  3989  sylan9ss  3992  ssdifss  4132  uneqin  4275  intss2  5106  ssrnres  6177  relrelss  6272  fcof  6741  fcoOLD  6743  fssres  6758  ssimaex  6978  dff3  7105  tpostpos2  8247  smores  8367  om00  8590  omeulem2  8598  cofonr  8689  naddunif  8708  pmss12g  8882  unblem1  9314  unblem2  9315  unblem3  9316  unblem4  9317  isfinite2  9320  cantnfval2  9687  cantnfle  9689  rankxplim3  9899  alephinit  10113  dfac12lem2  10162  ackbij1lem11  10248  cfeq0  10274  cfsuc  10275  cff1  10276  cflim2  10281  cfss  10283  cfslb2n  10286  cofsmo  10287  cfsmolem  10288  fin23lem34  10364  fin1a2lem13  10430  axdc3lem2  10469  axdclem  10537  pwcfsdom  10601  wunfi  10739  tskxpss  10790  tskcard  10799  suprzcl  12667  uzwo  12920  uzwo2  12921  infssuzle  12940  infssuzcl  12941  supxrbnd  13334  supxrgtmnf  13335  supxrre1  13336  supxrre2  13337  supxrss  13338  infxrss  13345  iccsupr  13446  hashf1lem2  14444  trclun  14988  fsum2d  15744  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fprod2d  15952  rpnnen2lem4  16188  rpnnen2lem7  16191  ramub2  16977  ressinbas  17220  ressress  17223  submre  17579  mrcss  17590  mreacs  17632  drsdirfi  18291  clatglbss  18505  ipopos  18522  cntz2ss  19280  pgrpsubgsymg  19358  ablfac1eulem  20023  subrngint  20491  subrgint  20528  tgval  22852  mretopd  22990  ssnei  23008  opnneiss  23016  restdis  23076  restcls  23079  restntr  23080  tgcnp  23151  fbssfi  23735  fgss2  23772  fgcl  23776  supfil  23793  alexsubALTlem3  23947  alexsubALTlem4  23948  cnextcn  23965  ustex3sym  24116  trust  24128  restutop  24136  utop2nei  24149  cfiluweak  24194  blssexps  24326  blssex  24327  mopni3  24397  metss  24411  metcnp3  24443  metust  24461  cfilucfil  24462  psmetutop  24470  tgioo  24706  xrsmopn  24722  fsumcn  24782  cncfmptid  24827  iscmet3lem2  25214  caussi  25219  ovolsslem  25407  ovolsscl  25409  ovolssnul  25410  opnmblALT  25526  itgfsum  25750  limcresi  25808  dvmptfsum  25901  plyss  26127  madebdayim  27808  cofcutrtime  27841  nbuhgr  29150  chsupunss  31148  shsupunss  31150  spanss  31152  shslubi  31189  shlub  31218  mdsl1i  32125  mdsl2i  32126  cvmdi  32128  mdslmd1lem1  32129  mdslmd1lem2  32130  mdslmd2i  32134  mdslmd4i  32137  atomli  32186  atcvatlem  32189  chirredlem2  32195  chirredi  32198  mdsymlem5  32211  xrge0infss  32525  tpr2rico  33508  sigainb  33750  dya2icoseg2  33893  omssubadd  33915  eulerpartlemn  33996  ballotlem2  34103  nummin  34709  cvmlift2lem12  34919  opnbnd  35804  fneint  35827  dissneqlem  36814  inunissunidif  36849  pibt2  36891  fin2so  37075  matunitlindflem1  37084  mblfinlem4  37128  ismblfin  37129  filbcmb  37208  heiborlem10  37288  igenmin  37532  lssatle  38482  paddss1  39285  paddss2  39286  paddss12  39287  paddssw2  39312  pclssN  39362  pclfinN  39368  polsubN  39375  2polvalN  39382  2polssN  39383  3polN  39384  2pmaplubN  39394  pnonsingN  39401  polsubclN  39420  dihord6apre  40724  dochsscl  40836  mapdordlem2  41105  isnacs3  42121  itgoss  42578  ofoaid1  42778  ofoaid2  42779  sspwimp  44348  sspwimpVD  44349  nsstr  44452  islptre  44998  gsumlsscl  47438  lincellss  47485  ellcoellss  47494

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »