Theorem sseqtrrd 3973

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  3sstr4d  3991  fssrescdmd  7081  funfvima2d  7188  fnfvima  7189  frrlem8  8245  frrlem10  8247  fprresex  8262  oaordi  8483  omordi  8503  omlimcl  8515  oen0  8524  domunsncan  9017  f1opwfi  9268  cantnfle  9592  cantnflt  9593  cantnflem1d  9609  ttrcltr  9637  r1pwss  9708  rankxplim3  9805  acndom2  9976  fodomfi2  9982  cflm  10172  cflim2  10185  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  axdc2lem  10370  ttukeylem5  10435  wunex2  10661  ssfzunsn  13498  ccatass  14524  swrdval2  14582  splfv2a  14691  revccat  14701  cshimadifsn  14764  cshimadifsn0  14765  rtrclreclem1  14992  rtrclreclem2  14994  sumrblem  15646  prodrblem  15864  dfphi2  16713  vdwlem1  16921  basprssdmsets  17160  imasaddfnlem  17461  imasaddvallem  17462  imasvscafn  17470  imasvscaval  17471  mreexexlem4d  17582  mreexfidimd  17585  sscpwex  17751  acsmap2d  18490  gsumress  18619  subsubmgm  18647  subsubm  18753  frmdsssubm  18798  frmdss2  18800  subsubg  19091  cntzmhm2  19283  cntzcmnf  19786  ablcntzd  19798  gsumzsubmcl  19859  gsumconst  19875  gsumzmhm  19878  subgdmdprd  19977  dprdcntz2  19981  dprd2da  19985  dmdprdsplit2lem  19988  ablfac1eu  20016  pgpfaclem1  20024  pgpfaclem2  20025  subsubrng  20508  subsubrg  20543  issubdrg  20725  subdrgint  20748  lmhmlsp  21013  lspsntri  21061  lspindpi  21099  lidldvgen  21301  gsumfsum  21401  mrccss  21661  frlmsslsp  21763  opsrtoslem2  22023  ressply1evl  22326  scmatsgrp1  22478  toponss  22883  ssntr  23014  elcls3  23039  toponmre  23049  neiptoptop  23087  neiptopnei  23088  neitr  23136  ordtbas  23148  ordtopn1  23150  ordtopn2  23151  iscnp3  23200  tgcn  23208  tgcnp  23209  ssidcn  23211  cnclsi  23228  cncls  23230  cncnp  23236  lmcld  23259  tgcmp  23357  cnconn  23378  connima  23381  clsconn  23386  conncompcld  23390  1stccnp  23418  kgentopon  23494  llycmpkgen2  23506  1stckgen  23510  kgencn2  23513  ptopn  23539  txcls  23560  ptpjcn  23567  ptclsg  23571  xkoccn  23575  txcnp  23576  ptcnplem  23577  txcmplem2  23598  xkoptsub  23610  xkopt  23611  xkoco2cn  23614  xkococnlem  23615  xkoinjcn  23643  imasnopn  23646  imasncld  23647  imasncls  23648  qtopkgen  23666  basqtop  23667  tgqtop  23668  qtoprest  23673  kqsat  23687  kqcldsat  23689  kqnrmlem1  23699  kqnrmlem2  23700  hmeontr  23725  reghmph  23749  nrmhmph  23750  fmfnfmlem4  23913  fmfnfm  23914  flimopn  23931  flimclslem  23940  flfnei  23947  lmflf  23961  txflf  23962  fclsopn  23970  fclsfnflim  23983  alexsublem  24000  ptcmplem3  24010  cnextcn  24023  efmndtmd  24057  submtmd  24060  subgtgp  24061  symgtgp  24062  clssubg  24065  clsnsg  24066  tgpconncompeqg  24068  snclseqg  24072  tsmscls  24094  trust  24185  restutop  24193  restutopopn  24194  utop3cls  24207  utopreg  24208  trcfilu  24249  blssec  24391  prdsbl  24447  blssopn  24451  metcnp  24497  cfilucfil  24515  psmetutop  24523  iccntr  24778  icccmplem2  24780  reconnlem1  24783  metnrmlem1a  24815  metnrmlem1  24816  metnrmlem2  24817  metnrmlem3  24818  cnheibor  24922  lebnumlem1  24928  lebnumlem3  24930  lebnumii  24933  clsocv  25218  iscfil2  25234  iscmet3  25261  cmetss  25284  relcmpcmet  25286  bcthlem5  25296  itg1addlem5  25669  perfdvf  25872  dvres3  25882  dvres3a  25883  dvcmul  25915  dvcmulf  25916  dvlip2  25968  lhop1lem  25986  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcnvre  25992  dvcvx  25993  plyco0  26165  plyaddlem1  26186  plymullem1  26187  aalioulem3  26310  ulmdvlem1  26377  precsexlem6  28220  precsexlem7  28221  bdayn0p1  28377  bdaypw2n0bndlem  28471  z12bdaylem2  28479  axcontlem10  29058  eengtrkg  29071  wlkp1lem7  29763  cyclnumvtx  29885  1wlkdlem4  30227  hsupunss  31430  pjpjpre  31506  ssmd2  32399  superpos  32441  atexch  32468  curry2ima  32798  pfxf1  33034  gsumhashmul  33160  symgcom2  33177  pmtrcnelor  33184  cycpmco2lem7  33225  cycpmconjvlem  33234  cycpmconjv  33235  cyc3conja  33250  elrgspnsubrunlem2  33341  subsdrg  33391  nsgmgc  33504  nsgqusf1olem3  33507  elrspunidl  33520  mxidlprm  33562  rprmdvdsprod  33626  dfufd2lem  33641  esplyfvaln  33750  lssdimle  33784  dimkerim  33804  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  dimlssid  33809  fldsdrgfldext2  33839  fldextrspunlsplem  33850  fldextrspunlsp  33851  fldextrspunlem1  33852  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  constr01  33919  constrmon  33921  constrextdg2lem  33925  constrext2chnlem  33927  madjusmdetlem2  34005  zarclsun  34047  rhmpreimacnlem  34061  ordtconnlem1  34101  measiuns  34394  imambfm  34439  cnmbfm  34440  dya2iocnrect  34458  omsfval  34471  omssubaddlem  34476  omssubadd  34477  totprobd  34603  fzssfzo  34716  signstfvn  34746  bnj999  35133  bnj1408  35211  bnj1442  35224  bnj1450  35225  bnj1501  35242  fnrelpredd  35266  revwlk  35338  cvmsss2  35487  cvmliftmolem1  35494  cvmliftlem3  35500  cvmlift2lem9  35524  cvmlift2lem11  35526  cvmlift3lem6  35537  cvmlift3lem7  35538  ssmclslem  35778  mclsax  35782  mclsppslem  35796  mclspps  35797  dfrdg2  36006  neiin  36545  neibastop2  36574  filnetlem4  36594  weiunfrlem  36677  rdgssun  37627  lindsdom  37859  poimirlem11  37876  poimirlem12  37877  itg2addnclem2  37917  cnres2  38008  sstotbnd2  38019  sstotbnd  38020  prdstotbnd  38039  heibor1lem  38054  igenval2  38311  lshpnelb  39354  lcvexchlem4  39407  lsatexch  39413  l1cvat  39425  lkrscss  39468  lkrss  39538  lkreqN  39540  paddunN  40297  osumcllem2N  40327  pmapojoinN  40338  pl42lem2N  40350  dibglbN  41536  diblss  41540  dicvaddcl  41560  dicvscacl  41561  diclss  41563  cdlemn5pre  41570  dihord5apre  41632  dihglblem3N  41665  dihglb2  41712  dochsat  41753  dochshpncl  41754  djhspss  41776  dihsumssj  41778  mapdlsm  42034  hdmaprnlem3eN  42228  hdmaplkr  42283  fnwe2lem2  43402  lnmlsslnm  43432  lmhmfgima  43435  hbtlem6  43480  omabs2  43683  tfsconcatrev  43699  naddwordnexlem0  43747  trrelsuperreldg  44018  iunrelexpuztr  44069  clsk1indlem2  44392  grumnudlem  44635  dvsconst  44680  dvsinax  46265  dvbdfbdioolem1  46280  itgsinexplem1  46306  itgperiod  46333  stoweidlem39  46391  dirkeritg  46454  fourierdlem48  46506  fourierdlem49  46507  fourierdlem70  46528  fourierdlem71  46529  fourierdlem81  46539  issalgend  46690  chnsubseqwl  47231  f1oresf1o  47644  clnbgrgrim  48288  rmsuppss  48724  restcls2lem  49266  iscnrm3rlem7  49299