Theorem sseqtrrd 4050

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  fssrescdmd  7160  funfvima2d  7269  fnfvima  7270  frrlem8  8334  frrlem10  8336  fprresex  8351  wfrlem17OLD  8381  oaordi  8602  omordi  8622  omlimcl  8634  oen0  8642  domunsncan  9138  f1opwfi  9426  cantnfle  9740  cantnflt  9741  cantnflem1d  9757  ttrcltr  9785  r1pwss  9853  rankxplim3  9950  acndom2  10123  fodomfi2  10129  cflm  10319  cflim2  10332  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  axdc2lem  10517  ttukeylem5  10582  wunex2  10807  ssfzunsn  13630  ccatass  14636  swrdval2  14694  splfv2a  14804  revccat  14814  cshimadifsn  14878  cshimadifsn0  14879  rtrclreclem1  15106  rtrclreclem2  15108  sumrblem  15759  prodrblem  15977  dfphi2  16821  vdwlem1  17028  basprssdmsets  17271  imasaddfnlem  17588  imasaddvallem  17589  imasvscafn  17597  imasvscaval  17598  mreexexlem4d  17705  mreexfidimd  17708  sscpwex  17876  acsmap2d  18625  gsumress  18720  subsubmgm  18748  subsubm  18851  frmdsssubm  18896  frmdss2  18898  subsubg  19189  cntzmhm2  19382  cntzcmnf  19887  ablcntzd  19899  gsumzsubmcl  19960  gsumconst  19976  gsumzmhm  19979  subgdmdprd  20078  dprdcntz2  20082  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1eu  20117  pgpfaclem1  20125  pgpfaclem2  20126  subsubrng  20589  subsubrg  20626  issubdrg  20803  subdrgint  20826  lmhmlsp  21071  lspsntri  21119  lspindpi  21157  lidldvgen  21367  gsumfsum  21475  mrccss  21735  frlmsslsp  21839  opsrtoslem2  22103  ressply1evl  22395  scmatsgrp1  22549  toponss  22954  ssntr  23087  elcls3  23112  toponmre  23122  neiptoptop  23160  neiptopnei  23161  neitr  23209  ordtbas  23221  ordtopn1  23223  ordtopn2  23224  iscnp3  23273  tgcn  23281  tgcnp  23282  ssidcn  23284  cnclsi  23301  cncls  23303  cncnp  23309  lmcld  23332  tgcmp  23430  cnconn  23451  connima  23454  clsconn  23459  conncompcld  23463  1stccnp  23491  kgentopon  23567  llycmpkgen2  23579  1stckgen  23583  kgencn2  23586  ptopn  23612  txcls  23633  ptpjcn  23640  ptclsg  23644  xkoccn  23648  txcnp  23649  ptcnplem  23650  txcmplem2  23671  xkoptsub  23683  xkopt  23684  xkoco2cn  23687  xkococnlem  23688  xkoinjcn  23716  imasnopn  23719  imasncld  23720  imasncls  23721  qtopkgen  23739  basqtop  23740  tgqtop  23741  qtoprest  23746  kqsat  23760  kqcldsat  23762  kqnrmlem1  23772  kqnrmlem2  23773  hmeontr  23798  reghmph  23822  nrmhmph  23823  fmfnfmlem4  23986  fmfnfm  23987  flimopn  24004  flimclslem  24013  flfnei  24020  lmflf  24034  txflf  24035  fclsopn  24043  fclsfnflim  24056  alexsublem  24073  ptcmplem3  24083  cnextcn  24096  efmndtmd  24130  submtmd  24133  subgtgp  24134  symgtgp  24135  clssubg  24138  clsnsg  24139  tgpconncompeqg  24141  snclseqg  24145  tsmscls  24167  trust  24259  restutop  24267  restutopopn  24268  utop3cls  24281  utopreg  24282  trcfilu  24324  blssec  24466  prdsbl  24525  blssopn  24529  metcnp  24575  cfilucfil  24593  psmetutop  24601  iccntr  24862  icccmplem2  24864  reconnlem1  24867  metnrmlem1a  24899  metnrmlem1  24900  metnrmlem2  24901  metnrmlem3  24902  cnheibor  25006  lebnumlem1  25012  lebnumlem3  25014  lebnumii  25017  clsocv  25303  iscfil2  25319  iscmet3  25346  cmetss  25369  relcmpcmet  25371  bcthlem5  25381  itg1addlem5  25755  perfdvf  25958  dvres3  25968  dvres3a  25969  dvcmul  26001  dvcmulf  26002  dvlip2  26054  lhop1lem  26072  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvcvx  26079  plyco0  26251  plyaddlem1  26272  plymullem1  26273  aalioulem3  26394  ulmdvlem1  26461  precsexlem6  28254  precsexlem7  28255  axcontlem10  29006  eengtrkg  29019  wlkp1lem7  29715  1wlkdlem4  30172  hsupunss  31375  pjpjpre  31451  ssmd2  32344  superpos  32386  atexch  32413  curry2ima  32720  pfxf1  32908  gsumhashmul  33040  symgcom2  33077  pmtrcnelor  33084  cycpmco2lem7  33125  cycpmconjvlem  33134  cycpmconjv  33135  cyc3conja  33150  nsgmgc  33405  nsgqusf1olem3  33408  elrspunidl  33421  mxidlprm  33463  rprmdvdsprod  33527  dfufd2lem  33542  lssdimle  33620  dimkerim  33640  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  dimlssid  33645  constr01  33732  constrmon  33734  madjusmdetlem2  33774  zarclsun  33816  rhmpreimacnlem  33830  ordtconnlem1  33870  measiuns  34181  imambfm  34227  cnmbfm  34228  dya2iocnrect  34246  omsfval  34259  omssubaddlem  34264  omssubadd  34265  totprobd  34391  fzssfzo  34516  signstfvn  34546  bnj999  34934  bnj1408  35012  bnj1442  35025  bnj1450  35026  bnj1501  35043  fnrelpredd  35065  revwlk  35092  cvmsss2  35242  cvmliftmolem1  35249  cvmliftlem3  35255  cvmlift2lem9  35279  cvmlift2lem11  35281  cvmlift3lem6  35292  cvmlift3lem7  35293  ssmclslem  35533  mclsax  35537  mclsppslem  35551  mclspps  35552  dfrdg2  35759  neiin  36298  neibastop2  36327  filnetlem4  36347  weiunfrlem  36430  rdgssun  37344  lindsdom  37574  poimirlem11  37591  poimirlem12  37592  itg2addnclem2  37632  cnres2  37723  sstotbnd2  37734  sstotbnd  37735  prdstotbnd  37754  heibor1lem  37769  igenval2  38026  lshpnelb  38940  lcvexchlem4  38993  lsatexch  38999  l1cvat  39011  lkrscss  39054  lkrss  39124  lkreqN  39126  paddunN  39884  osumcllem2N  39914  pmapojoinN  39925  pl42lem2N  39937  dibglbN  41123  diblss  41127  dicvaddcl  41147  dicvscacl  41148  diclss  41150  cdlemn5pre  41157  dihord5apre  41219  dihglblem3N  41252  dihglb2  41299  dochsat  41340  dochshpncl  41341  djhspss  41363  dihsumssj  41365  mapdlsm  41621  hdmaprnlem3eN  41815  hdmaplkr  41870  fnwe2lem2  43008  lnmlsslnm  43038  lmhmfgima  43041  hbtlem6  43086  omabs2  43294  tfsconcatrev  43310  naddwordnexlem0  43358  trrelsuperreldg  43630  iunrelexpuztr  43681  clsk1indlem2  44004  grumnudlem  44254  dvsconst  44299  dvsinax  45834  dvbdfbdioolem1  45849  itgsinexplem1  45875  itgperiod  45902  stoweidlem39  45960  dirkeritg  46023  fourierdlem48  46075  fourierdlem49  46076  fourierdlem70  46097  fourierdlem71  46098  fourierdlem81  46108  issalgend  46259  f1oresf1o  47205  clnbgrgrim  47786  rmsuppss  48095  restcls2lem  48592  iscnrm3rlem7  48626