Theorem sseqtrrd 3975

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 2769	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3974	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  3sstr4d  3993  fssrescdmd  7124  funfvima2d  7232  fnfvima  7233  frrlem8  8291  frrlem10  8293  fprresex  8308  oaordi  8532  omordi  8552  omlimcl  8564  oen0  8573  domunsncan  9066  f1opwfi  9314  cantnfle  9641  cantnflt  9642  cantnflem1d  9658  ttrcltr  9686  r1pwss  9757  rankxplim3  9854  acndom2  10039  fodomfi2  10045  cflm  10234  cflim2  10248  isf34lem5  10363  isf34lem7  10364  isf34lem6  10365  axdc2lem  10433  ttukeylem5  10498  wunex2  10724  ssfzunsn  13600  ccatass  14628  swrdval2  14686  splfv2a  14795  revccat  14805  cshimadifsn  14868  cshimadifsn0  14869  rtrclreclem1  15096  rtrclreclem2  15098  sumrblem  15764  prodrblem  15985  dfphi2  16834  vdwlem1  17042  basprssdmsets  17282  imasaddfnlem  17583  imasaddvallem  17584  imasvscafn  17592  imasvscaval  17593  mreexexlem4d  17704  mreexfidimd  17707  sscpwex  17873  acsmap2d  18612  gsumress  18741  subsubmgm  18769  subsubm  18876  frmdsssubm  18921  frmdss2  18923  subsubg  19217  cntzmhm2  19413  cntzcmnf  19916  ablcntzd  19928  gsumzsubmcl  19989  gsumconst  20005  gsumzmhm  20008  subgdmdprd  20107  dprdcntz2  20111  dprd2da  20115  dmdprdsplit2lem  20118  ablfac1eu  20146  pgpfaclem1  20154  pgpfaclem2  20155  subsubrng  20649  subsubrg  20684  issubdrg  20864  subdrgint  20887  lmhmlsp  21151  lspsntri  21199  lspindpi  21237  rspprop  21351  lidldvgen  21483  gsumfsum  21565  mrccss  21825  frlmsslsp  21927  opsrtoslem2  22188  ressply1evl  22511  scmatsgrp1  22660  toponss  23065  ssntr  23196  elcls3  23221  toponmre  23231  neiptoptop  23269  neiptopnei  23270  neitr  23318  ordtbas  23330  ordtopn1  23332  ordtopn2  23333  iscnp3  23382  tgcn  23390  tgcnp  23391  ssidcn  23393  cnclsi  23410  cncls  23412  cncnp  23418  lmcld  23441  tgcmp  23539  cnconn  23560  connima  23563  clsconn  23568  conncompcld  23572  1stccnp  23600  kgentopon  23676  llycmpkgen2  23688  1stckgen  23692  kgencn2  23695  ptopn  23721  txcls  23742  ptpjcn  23749  ptclsg  23753  xkoccn  23757  txcnp  23758  ptcnplem  23759  txcmplem2  23780  xkoptsub  23792  xkopt  23793  xkoco2cn  23796  xkococnlem  23797  xkoinjcn  23825  imasnopn  23828  imasncld  23829  imasncls  23830  qtopkgen  23848  basqtop  23849  tgqtop  23850  qtoprest  23855  kqsat  23869  kqcldsat  23871  kqnrmlem1  23881  kqnrmlem2  23882  hmeontr  23907  reghmph  23931  nrmhmph  23932  fmfnfmlem4  24095  fmfnfm  24096  flimopn  24113  flimclslem  24122  flfnei  24129  lmflf  24143  txflf  24144  fclsopn  24152  fclsfnflim  24165  alexsublem  24182  ptcmplem3  24192  cnextcn  24205  efmndtmd  24239  submtmd  24242  subgtgp  24243  symgtgp  24244  clssubg  24247  clsnsg  24248  tgpconncompeqg  24250  snclseqg  24254  tsmscls  24276  trust  24367  restutop  24375  restutopopn  24376  utop3cls  24389  utopreg  24390  trcfilu  24431  blssec  24573  prdsbl  24629  blssopn  24633  metcnp  24679  cfilucfil  24697  psmetutop  24705  iccntr  24960  icccmplem2  24962  reconnlem1  24965  metnrmlem1a  24997  metnrmlem1  24998  metnrmlem2  24999  metnrmlem3  25000  cnheibor  25095  lebnumlem1  25101  lebnumlem3  25103  lebnumii  25106  clsocv  25390  iscfil2  25406  iscmet3  25433  cmetss  25456  relcmpcmet  25458  bcthlem5  25468  itg1addlem5  25840  perfdvf  26043  dvres3  26053  dvres3a  26054  dvcmul  26084  dvcmulf  26085  dvlip2  26135  lhop1lem  26153  dvcnvrelem1  26157  dvcnvrelem2  26158  dvcnvre  26159  dvcvx  26160  plyco0  26330  plyaddlem1  26351  plymullem1  26352  aalioulem3  26476  ulmdvlem1  26541  precsexlem6  28383  precsexlem7  28384  bdayn0p1  28540  bdaypw2n0bndlem  28634  z12bdaylem2  28642  plngrotlem1  29047  lnssplnglem  29051  prlngpln4  29186  quadcgrprlng  29194  axcontlem10  29301  eengtrkg  29314  wlkp1lem7  30005  cyclnumvtx  30127  1wlkdlem4  30469  hsupunss  31673  pjpjpre  31749  ssmd2  32642  superpos  32684  atexch  32711  curry2ima  33032  pfxf1  33240  gsumhashmul  33365  symgcom2  33382  pmtrcnelor  33389  cycpmco2lem7  33430  cycpmconjvlem  33439  cycpmconjv  33440  cyc3conja  33455  elrgspnsubrunlem2  33546  subsdrg  33597  nsgmgc  33699  nsgqusf1olem3  33702  elrspunidl  33714  mxidlprm  33731  rprmdvdsprod  33802  dfufd2lem  33817  esplyfvaln  33942  lssdimle  33976  dimkerim  33995  fedgmullem1  33997  fedgmullem2  33998  fedgmul  33999  dimlssid  34000  fldsdrgfldext2  34030  fldextrspunlsplem  34041  fldextrspunlsp  34042  fldextrspunlem1  34043  fldextrspundgdvdslem  34048  fldextrspundgdvds  34049  constr01  34110  constrmon  34112  constrextdg2lem  34116  constrext2chnlem  34118  madjusmdetlem2  34196  zarclsun  34238  rhmpreimacnlem  34252  ordtconnlem1  34292  measiuns  34585  imambfm  34630  cnmbfm  34631  dya2iocnrect  34649  omsfval  34662  omssubaddlem  34667  omssubadd  34668  totprobd  34794  fzssfzo  34907  signstfvn  34934  bnj999  35324  bnj1408  35402  bnj1442  35415  bnj1450  35416  bnj1501  35433  fnrelpredd  35460  revwlk  35595  cvmsss2  35744  cvmliftmolem1  35751  cvmliftlem3  35757  cvmlift2lem9  35781  cvmlift2lem11  35783  cvmlift3lem6  35794  cvmlift3lem7  35795  ssmclslem  36035  mclsax  36039  mclsppslem  36053  mclspps  36054  dfrdg2  36263  neiin  36821  neibastop2  36850  filnetlem4  36870  weiunfrlem  36953  rdgssun  38002  lindsdom  38243  poimirlem11  38260  poimirlem12  38261  itg2addnclem2  38301  cnres2  38392  sstotbnd2  38403  sstotbnd  38404  prdstotbnd  38423  heibor1lem  38438  igenval2  38695  lshpnelb  39736  lcvexchlem4  39789  lsatexch  39795  l1cvat  39807  lkrscss  39850  lkrss  39920  lkreqN  39922  paddunN  40679  osumcllem2N  40709  pmapojoinN  40720  pl42lem2N  40732  dibglbN  41918  diblss  41922  dicvaddcl  41942  dicvscacl  41943  diclss  41945  cdlemn5pre  41952  dihord5apre  42014  dihglblem3N  42047  dihglb2  42094  dochsat  42135  dochshpncl  42136  djhspss  42158  dihsumssj  42160  mapdlsm  42416  hdmaprnlem3eN  42610  hdmaplkr  42665  fnwe2lem2  43758  lnmlsslnm  43788  lmhmfgima  43791  hbtlem6  43836  omabs2  44039  tfsconcatrev  44055  naddwordnexlem0  44103  trrelsuperreldg  44374  iunrelexpuztr  44425  clsk1indlem2  44748  grumnudlem  44975  dvsconst  45020  dvsinax  46607  dvbdfbdioolem1  46622  itgsinexplem1  46648  itgperiod  46675  stoweidlem39  46733  dirkeritg  46796  fourierdlem48  46848  fourierdlem49  46849  fourierdlem70  46870  fourierdlem71  46871  fourierdlem81  46881  issalgend  47032  chnsubseqwl  47575  f1oresf1o  48004  clnbgrgrim  48676  rmsuppss  49127  restcls2lem  49668  iscnrm3rlem7  49701