Theorem sseqtrrd 3968

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  3sstr4d  3986  fssrescdmd  7119  funfvima2d  7230  fnfvima  7231  frrlem8  8295  frrlem10  8297  fprresex  8312  oaordi  8538  omordi  8558  omlimcl  8570  oen0  8579  domunsncan  9080  f1opwfi  9329  cantnfle  9656  cantnflt  9657  cantnflem1d  9673  ttrcltr  9701  r1pwss  9774  rankxplim3  9879  acndom2  10114  fodomfi2  10120  cflm  10308  cflim2  10322  isf34lem5  10437  isf34lem7  10438  isf34lem6  10439  axdc2lem  10507  ttukeylem5  10572  wunex2  10804  ssfzunsn  13684  ccatass  14714  swrdval2  14774  splfv2a  14885  revccat  14895  cshimadifsn  14960  cshimadifsn0  14961  rtrclreclem1  15190  rtrclreclem2  15192  sumrblem  15857  prodrblem  16076  dfphi2  16931  vdwlem1  17139  basprssdmsets  17379  imasaddfnlem  17680  imasaddvallem  17681  imasvscafn  17689  imasvscaval  17690  mreexexlem4d  17801  mreexfidimd  17804  sscpwex  17970  acsmap2d  18709  gsumress  18851  subsubmgm  18879  subsubm  18992  frmdsssubm  19037  frmdss2  19039  subsubg  19340  cntzmhm2  19536  cntzcmnf  20039  ablcntzd  20051  gsumzsubmcl  20112  gsumconst  20128  gsumzmhm  20131  subgdmdprd  20230  dprdcntz2  20234  dprd2da  20238  dmdprdsplit2lem  20241  ablfac1eu  20269  pgpfaclem1  20277  pgpfaclem2  20278  subsubrng  20795  subsubrg  20830  issubdrg  21017  subdrgint  21040  lmhmlsp  21304  lspsntri  21352  lspindpi  21390  rspprop  21504  lidldvgen  21638  gsumfsum  21720  mrccss  21980  frlmsslsp  22082  lindsdom  22136  opsrtoslem2  22345  ressply1evl  22668  scmatsgrp1  22817  toponss  23225  ssntr  23356  elcls3  23381  toponmre  23391  neiptoptop  23429  neiptopnei  23430  neitr  23478  ordtbas  23490  ordtopn1  23492  ordtopn2  23493  iscnp3  23542  tgcn  23550  tgcnp  23551  ssidcn  23553  cnclsi  23570  cncls  23572  cncnp  23578  lmcld  23601  tgcmp  23699  cnconn  23720  connima  23723  clsconn  23728  conncompcld  23732  1stccnp  23761  kgentopon  23837  llycmpkgen2  23849  1stckgen  23853  kgencn2  23856  ptopn  23882  txcls  23903  ptpjcn  23910  ptclsg  23914  xkoccn  23918  txcnp  23919  ptcnplem  23920  txcmplem2  23941  xkoptsub  23953  xkopt  23954  xkoco2cn  23957  xkococnlem  23958  xkoinjcn  23986  imasnopn  23989  imasncld  23990  imasncls  23991  qtopkgen  24009  basqtop  24010  tgqtop  24011  qtoprest  24016  kqsat  24030  kqcldsat  24032  kqnrmlem1  24042  kqnrmlem2  24043  hmeontr  24068  reghmph  24092  nrmhmph  24093  fmfnfmlem4  24256  fmfnfm  24257  flimopn  24274  flimclslem  24283  flfnei  24290  lmflf  24304  txflf  24305  fclsopn  24313  fclsfnflim  24326  alexsublem  24343  ptcmplem3  24353  cnextcn  24366  efmndtmd  24400  submtmd  24403  subgtgp  24404  symgtgp  24405  clssubg  24408  clsnsg  24409  tgpconncompeqg  24411  snclseqg  24415  tsmscls  24437  trust  24528  restutop  24536  restutopopn  24537  utop3cls  24550  utopreg  24551  trcfilu  24592  blssec  24734  prdsbl  24790  blssopn  24794  metcnp  24840  cfilucfil  24858  psmetutop  24866  iccntr  25121  icccmplem2  25123  reconnlem1  25126  metnrmlem1a  25158  metnrmlem1  25159  metnrmlem2  25160  metnrmlem3  25161  cnheibor  25256  lebnumlem1  25262  lebnumlem3  25264  lebnumii  25267  clsocv  25551  iscfil2  25567  iscmet3  25594  cmetss  25617  relcmpcmet  25619  bcthlem5  25629  itg1addlem5  26001  perfdvf  26203  dvres3  26213  dvres3a  26214  dvcmul  26244  dvcmulf  26245  dvlip2  26295  lhop1lem  26313  dvcnvrelem1  26317  dvcnvrelem2  26318  dvcnvre  26319  dvcvx  26320  plyco0  26490  plyaddlem1  26512  plymullem1  26513  aalioulem3  26643  ulmdvlem1  26709  precsexlem6  28580  precsexlem7  28581  bdayn0p1  28737  bdaypw2n0bndlem  28831  z12bdaylem2  28839  plngrotlem1  29247  lnssplnglem  29251  prlngpln4  29418  quadcgrprlng  29426  axcontlem10  29533  eengtrkg  29546  wlkp1lem7  30240  revwlk  30249  cyclnumvtx  30370  1wlkdlem4  30713  hsupunss  31927  pjpjpre  32003  ssmd2  32896  superpos  32938  atexch  32965  curry2ima  33284  pfxf1  33491  gsumhashmul  33610  symgcom2  33627  pmtrcnelor  33634  cycpmco2lem7  33675  cycpmconjvlem  33684  cycpmconjv  33685  cyc3conja  33700  elrgspnsubrunlem2  33791  subsdrg  33842  nsgmgc  33945  nsgqusf1olem3  33948  elrspunidl  33960  mxidlprm  33977  rprmdvdsprod  34048  dfufd2lem  34063  esplyfvaln  34188  lssdimle  34222  dimkerim  34241  fedgmullem1  34243  fedgmullem2  34244  fedgmul  34245  dimlssid  34246  fldsdrgfldext2  34276  fldextrspunlsplem  34287  fldextrspunlsp  34288  fldextrspunlem1  34289  fldextrspundgdvdslem  34294  fldextrspundgdvds  34295  constr01  34356  constrmon  34358  constrextdg2lem  34362  constrext2chnlem  34364  madjusmdetlem2  34442  zarclsun  34484  rhmpreimacnlem  34498  ordtconnlem1  34538  measiuns  34832  imambfm  34877  cnmbfm  34878  dya2iocnrect  34896  omsfval  34909  omssubaddlem  34914  omssubadd  34915  totprobd  35041  fzssfzo  35154  signstfvn  35181  bnj999  35571  bnj1408  35649  bnj1442  35662  bnj1450  35663  bnj1501  35680  fnrelpredd  35699  cvmsss2  36008  cvmliftmolem1  36015  cvmliftlem3  36021  cvmlift2lem9  36045  cvmlift2lem11  36047  cvmlift3lem6  36058  cvmlift3lem7  36059  ssmclslem  36299  mclsax  36303  mclsppslem  36317  mclspps  36318  dfrdg2  36527  neiin  37090  neibastop2  37119  filnetlem4  37139  weiunfrlem  37222  rdgssun  38269  poimirlem11  38517  poimirlem12  38518  itg2addnclem2  38558  cnres2  38665  sstotbnd2  38676  sstotbnd  38677  prdstotbnd  38696  heibor1lem  38711  igenval2  38968  lshpnelb  40009  lcvexchlem4  40062  lsatexch  40068  l1cvat  40080  lkrscss  40123  lkrss  40193  lkreqN  40195  paddunN  40952  osumcllem2N  40982  pmapojoinN  40993  pl42lem2N  41005  dibglbN  42191  diblss  42195  dicvaddcl  42215  dicvscacl  42216  diclss  42218  cdlemn5pre  42225  dihord5apre  42287  dihglblem3N  42320  dihglb2  42367  dochsat  42408  dochshpncl  42409  djhspss  42431  dihsumssj  42433  mapdlsm  42689  hdmaprnlem3eN  42883  hdmaplkr  42938  fnwe2lem2  44011  lnmlsslnm  44041  lmhmfgima  44044  hbtlem6  44089  omabs2  44292  tfsconcatrev  44308  naddwordnexlem0  44356  trrelsuperreldg  44627  iunrelexpuztr  44678  clsk1indlem2  45001  grumnudlem  45228  dvsconst  45273  dvsinax  46867  dvbdfbdioolem1  46882  itgsinexplem1  46908  itgperiod  46935  stoweidlem39  46993  dirkeritg  47056  fourierdlem48  47108  fourierdlem49  47109  fourierdlem70  47130  fourierdlem71  47131  fourierdlem81  47141  issalgend  47292  chnsubseqwl  47833  tmachlem-agreeprod  47891  f1oresf1o  48304  clnbgrgrim  48976  rmsuppss  49426  restcls2lem  49965  iscnrm3rlem7  49998