Theorem sseqtrrd 3987

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
sseqtrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2736	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3986	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  3sstr4d  4005  fssrescdmd  7101  funfvima2d  7209  fnfvima  7210  frrlem8  8275  frrlem10  8277  fprresex  8292  oaordi  8513  omordi  8533  omlimcl  8545  oen0  8553  domunsncan  9046  f1opwfi  9314  cantnfle  9631  cantnflt  9632  cantnflem1d  9648  ttrcltr  9676  r1pwss  9744  rankxplim3  9841  acndom2  10014  fodomfi2  10020  cflm  10210  cflim2  10223  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  axdc2lem  10408  ttukeylem5  10473  wunex2  10698  ssfzunsn  13538  ccatass  14560  swrdval2  14618  splfv2a  14728  revccat  14738  cshimadifsn  14802  cshimadifsn0  14803  rtrclreclem1  15030  rtrclreclem2  15032  sumrblem  15684  prodrblem  15902  dfphi2  16751  vdwlem1  16959  basprssdmsets  17198  imasaddfnlem  17498  imasaddvallem  17499  imasvscafn  17507  imasvscaval  17508  mreexexlem4d  17615  mreexfidimd  17618  sscpwex  17784  acsmap2d  18521  gsumress  18616  subsubmgm  18644  subsubm  18750  frmdsssubm  18795  frmdss2  18797  subsubg  19088  cntzmhm2  19281  cntzcmnf  19782  ablcntzd  19794  gsumzsubmcl  19855  gsumconst  19871  gsumzmhm  19874  subgdmdprd  19973  dprdcntz2  19977  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1eu  20012  pgpfaclem1  20020  pgpfaclem2  20021  subsubrng  20479  subsubrg  20514  issubdrg  20696  subdrgint  20719  lmhmlsp  20963  lspsntri  21011  lspindpi  21049  lidldvgen  21251  gsumfsum  21358  mrccss  21610  frlmsslsp  21712  opsrtoslem2  21970  ressply1evl  22264  scmatsgrp1  22416  toponss  22821  ssntr  22952  elcls3  22977  toponmre  22987  neiptoptop  23025  neiptopnei  23026  neitr  23074  ordtbas  23086  ordtopn1  23088  ordtopn2  23089  iscnp3  23138  tgcn  23146  tgcnp  23147  ssidcn  23149  cnclsi  23166  cncls  23168  cncnp  23174  lmcld  23197  tgcmp  23295  cnconn  23316  connima  23319  clsconn  23324  conncompcld  23328  1stccnp  23356  kgentopon  23432  llycmpkgen2  23444  1stckgen  23448  kgencn2  23451  ptopn  23477  txcls  23498  ptpjcn  23505  ptclsg  23509  xkoccn  23513  txcnp  23514  ptcnplem  23515  txcmplem2  23536  xkoptsub  23548  xkopt  23549  xkoco2cn  23552  xkococnlem  23553  xkoinjcn  23581  imasnopn  23584  imasncld  23585  imasncls  23586  qtopkgen  23604  basqtop  23605  tgqtop  23606  qtoprest  23611  kqsat  23625  kqcldsat  23627  kqnrmlem1  23637  kqnrmlem2  23638  hmeontr  23663  reghmph  23687  nrmhmph  23688  fmfnfmlem4  23851  fmfnfm  23852  flimopn  23869  flimclslem  23878  flfnei  23885  lmflf  23899  txflf  23900  fclsopn  23908  fclsfnflim  23921  alexsublem  23938  ptcmplem3  23948  cnextcn  23961  efmndtmd  23995  submtmd  23998  subgtgp  23999  symgtgp  24000  clssubg  24003  clsnsg  24004  tgpconncompeqg  24006  snclseqg  24010  tsmscls  24032  trust  24124  restutop  24132  restutopopn  24133  utop3cls  24146  utopreg  24147  trcfilu  24188  blssec  24330  prdsbl  24386  blssopn  24390  metcnp  24436  cfilucfil  24454  psmetutop  24462  iccntr  24717  icccmplem2  24719  reconnlem1  24722  metnrmlem1a  24754  metnrmlem1  24755  metnrmlem2  24756  metnrmlem3  24757  cnheibor  24861  lebnumlem1  24867  lebnumlem3  24869  lebnumii  24872  clsocv  25157  iscfil2  25173  iscmet3  25200  cmetss  25223  relcmpcmet  25225  bcthlem5  25235  itg1addlem5  25608  perfdvf  25811  dvres3  25821  dvres3a  25822  dvcmul  25854  dvcmulf  25855  dvlip2  25907  lhop1lem  25925  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvcvx  25932  plyco0  26104  plyaddlem1  26125  plymullem1  26126  aalioulem3  26249  ulmdvlem1  26316  precsexlem6  28121  precsexlem7  28122  bdayn0p1  28265  axcontlem10  28907  eengtrkg  28920  wlkp1lem7  29614  cyclnumvtx  29737  1wlkdlem4  30076  hsupunss  31279  pjpjpre  31355  ssmd2  32248  superpos  32290  atexch  32317  curry2ima  32639  pfxf1  32870  gsumhashmul  33008  symgcom2  33048  pmtrcnelor  33055  cycpmco2lem7  33096  cycpmconjvlem  33105  cycpmconjv  33106  cyc3conja  33121  elrgspnsubrunlem2  33206  subsdrg  33255  nsgmgc  33390  nsgqusf1olem3  33393  elrspunidl  33406  mxidlprm  33448  rprmdvdsprod  33512  dfufd2lem  33527  lssdimle  33610  dimkerim  33630  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  dimlssid  33635  fldsdrgfldext2  33665  fldextrspunlsplem  33675  fldextrspunlsp  33676  fldextrspunlem1  33677  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  constr01  33739  constrmon  33741  constrextdg2lem  33745  constrext2chnlem  33747  madjusmdetlem2  33825  zarclsun  33867  rhmpreimacnlem  33881  ordtconnlem1  33921  measiuns  34214  imambfm  34260  cnmbfm  34261  dya2iocnrect  34279  omsfval  34292  omssubaddlem  34297  omssubadd  34298  totprobd  34424  fzssfzo  34537  signstfvn  34567  bnj999  34955  bnj1408  35033  bnj1442  35046  bnj1450  35047  bnj1501  35064  fnrelpredd  35086  revwlk  35119  cvmsss2  35268  cvmliftmolem1  35275  cvmliftlem3  35281  cvmlift2lem9  35305  cvmlift2lem11  35307  cvmlift3lem6  35318  cvmlift3lem7  35319  ssmclslem  35559  mclsax  35563  mclsppslem  35577  mclspps  35578  dfrdg2  35790  neiin  36327  neibastop2  36356  filnetlem4  36376  weiunfrlem  36459  rdgssun  37373  lindsdom  37615  poimirlem11  37632  poimirlem12  37633  itg2addnclem2  37673  cnres2  37764  sstotbnd2  37775  sstotbnd  37776  prdstotbnd  37795  heibor1lem  37810  igenval2  38067  lshpnelb  38984  lcvexchlem4  39037  lsatexch  39043  l1cvat  39055  lkrscss  39098  lkrss  39168  lkreqN  39170  paddunN  39928  osumcllem2N  39958  pmapojoinN  39969  pl42lem2N  39981  dibglbN  41167  diblss  41171  dicvaddcl  41191  dicvscacl  41192  diclss  41194  cdlemn5pre  41201  dihord5apre  41263  dihglblem3N  41296  dihglb2  41343  dochsat  41384  dochshpncl  41385  djhspss  41407  dihsumssj  41409  mapdlsm  41665  hdmaprnlem3eN  41859  hdmaplkr  41914  fnwe2lem2  43047  lnmlsslnm  43077  lmhmfgima  43080  hbtlem6  43125  omabs2  43328  tfsconcatrev  43344  naddwordnexlem0  43392  trrelsuperreldg  43664  iunrelexpuztr  43715  clsk1indlem2  44038  grumnudlem  44281  dvsconst  44326  dvsinax  45918  dvbdfbdioolem1  45933  itgsinexplem1  45959  itgperiod  45986  stoweidlem39  46044  dirkeritg  46107  fourierdlem48  46159  fourierdlem49  46160  fourierdlem70  46181  fourierdlem71  46182  fourierdlem81  46192  issalgend  46343  f1oresf1o  47295  clnbgrgrim  47938  rmsuppss  48362  restcls2lem  48905  iscnrm3rlem7  48938