Theorem sseqtrrd 3950

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 3949	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3sstr4d  3968  fssrescdmd  7151  funfvima2d  7261  fnfvima  7262  frrlem8  8339  frrlem10  8341  fprresex  8356  oaordi  8582  omordi  8602  omlimcl  8614  oen0  8623  domunsncan  9124  f1opwfi  9373  cantnfle  9699  cantnflt  9700  cantnflem1d  9716  ttrcltr  9744  r1pwss  9818  rankxplim3  9925  acndom2  10160  fodomfi2  10166  cflm  10354  cflim2  10368  isf34lem5  10483  isf34lem7  10484  isf34lem6  10485  axdc2lem  10553  ttukeylem5  10618  wunex2  10850  ssfzunsn  13731  ccatass  14761  swrdval2  14822  splfv2a  14933  revccat  14943  cshimadifsn  15008  cshimadifsn0  15009  rtrclreclem1  15239  rtrclreclem2  15241  sumrblem  15906  prodrblem  16125  dfphi2  16980  vdwlem1  17188  basprssdmsets  17428  imasaddfnlem  17729  imasaddvallem  17730  imasvscafn  17738  imasvscaval  17739  mreexexlem4d  17850  mreexfidimd  17853  sscpwex  18019  acsmap2d  18758  gsumress  18900  subsubmgm  18928  subsubm  19041  frmdsssubm  19086  frmdss2  19088  subsubg  19389  cntzmhm2  19586  cntzcmnf  20089  ablcntzd  20101  gsumzsubmcl  20162  gsumconst  20178  gsumzmhm  20181  subgdmdprd  20280  dprdcntz2  20284  dprd2da  20288  dmdprdsplit2lem  20291  ablfac1eu  20319  pgpfaclem1  20327  pgpfaclem2  20328  subsubrng  20845  subsubrg  20880  issubdrg  21067  subdrgint  21090  lmhmlsp  21354  lspsntri  21402  lspindpi  21440  rspprop  21554  lidldvgen  21688  gsumfsum  21770  mrccss  22030  frlmsslsp  22132  lindsdom  22186  opsrtoslem2  22395  ressply1evl  22718  scmatsgrp1  22867  toponss  23275  ssntr  23406  elcls3  23431  toponmre  23441  neiptoptop  23479  neiptopnei  23480  neitr  23528  ordtbas  23540  ordtopn1  23542  ordtopn2  23543  iscnp3  23592  tgcn  23600  tgcnp  23601  ssidcn  23603  cnclsi  23620  cncls  23622  cncnp  23628  lmcld  23651  tgcmp  23749  cnconn  23770  connima  23773  clsconn  23778  conncompcld  23782  1stccnp  23811  kgentopon  23887  llycmpkgen2  23899  1stckgen  23903  kgencn2  23906  ptopn  23932  txcls  23953  ptpjcn  23960  ptclsg  23964  xkoccn  23968  txcnp  23969  ptcnplem  23970  txcmplem2  23991  xkoptsub  24003  xkopt  24004  xkoco2cn  24007  xkococnlem  24008  xkoinjcn  24036  imasnopn  24039  imasncld  24040  imasncls  24041  qtopkgen  24059  basqtop  24060  tgqtop  24061  qtoprest  24066  kqsat  24080  kqcldsat  24082  kqnrmlem1  24092  kqnrmlem2  24093  hmeontr  24118  reghmph  24142  nrmhmph  24143  fmfnfmlem4  24306  fmfnfm  24307  flimopn  24324  flimclslem  24333  flfnei  24340  lmflf  24354  txflf  24355  fclsopn  24363  fclsfnflim  24376  alexsublem  24393  ptcmplem3  24403  cnextcn  24416  efmndtmd  24450  submtmd  24453  subgtgp  24454  symgtgp  24455  clssubg  24458  clsnsg  24459  tgpconncompeqg  24461  snclseqg  24465  tsmscls  24487  trust  24578  restutop  24586  restutopopn  24587  utop3cls  24600  utopreg  24601  trcfilu  24642  blssec  24784  prdsbl  24840  blssopn  24844  metcnp  24890  cfilucfil  24908  psmetutop  24916  iccntr  25171  icccmplem2  25173  reconnlem1  25176  metnrmlem1a  25208  metnrmlem1  25209  metnrmlem2  25210  metnrmlem3  25211  cnheibor  25306  lebnumlem1  25312  lebnumlem3  25314  lebnumii  25317  clsocv  25601  iscfil2  25617  iscmet3  25644  cmetss  25667  relcmpcmet  25669  bcthlem5  25679  itg1addlem5  26051  perfdvf  26253  dvres3  26263  dvres3a  26264  dvcmul  26294  dvcmulf  26295  dvlip2  26345  lhop1lem  26363  dvcnvrelem1  26367  dvcnvrelem2  26368  dvcnvre  26369  dvcvx  26370  plyco0  26540  plyaddlem1  26562  plymullem1  26563  aalioulem3  26691  ulmdvlem1  26757  precsexlem6  28628  precsexlem7  28629  bdayn0p1  28785  bdaypw2n0bndlem  28879  z12bdaylem2  28887  plngrotlem1  29295  lnssplnglem  29299  prlngpln4  29466  quadcgrprlng  29474  axcontlem10  29581  eengtrkg  29594  wlkp1lem7  30288  revwlk  30297  cyclnumvtx  30418  1wlkdlem4  30761  hsupunss  31975  pjpjpre  32051  ssmd2  32944  superpos  32986  atexch  33013  curry2ima  33373  pfxf1  33579  gsumhashmul  33698  symgcom2  33715  pmtrcnelor  33722  cycpmco2lem7  33763  cycpmconjvlem  33772  cycpmconjv  33773  cyc3conja  33788  elrgspnsubrunlem2  33879  subsdrg  33930  nsgmgc  34033  nsgqusf1olem3  34036  elrspunidl  34048  mxidlprm  34065  rprmdvdsprod  34136  dfufd2lem  34151  esplyfvaln  34276  lssdimle  34310  dimkerim  34329  fedgmullem1  34331  fedgmullem2  34332  fedgmul  34333  dimlssid  34334  fldsdrgfldext2  34364  fldextrspunlsplem  34375  fldextrspunlsp  34376  fldextrspunlem1  34377  fldextrspundgdvdslem  34382  fldextrspundgdvds  34383  constr01  34444  constrmon  34446  constrextdg2lem  34450  constrext2chnlem  34452  madjusmdetlem2  34530  zarclsun  34572  rhmpreimacnlem  34586  ordtconnlem1  34626  measiuns  34920  imambfm  34964  cnmbfm  34965  dya2iocnrect  34983  omsfval  34996  omssubaddlem  35001  omssubadd  35002  totprobd  35128  fzssfzo  35241  signstfvn  35268  bnj999  35658  bnj1408  35736  bnj1442  35749  bnj1450  35750  bnj1501  35767  fnrelpredd  35804  cvmsss2  36206  cvmliftmolem1  36213  cvmliftlem3  36219  cvmlift2lem9  36243  cvmlift2lem11  36245  cvmlift3lem6  36256  cvmlift3lem7  36257  ssmclslem  36497  mclsax  36501  mclsppslem  36515  mclspps  36516  dfrdg2  36735  neiin  37298  neibastop2  37327  filnetlem4  37347  weiunfrlem  37430  rdgssun  38493  poimirlem11  38741  poimirlem12  38742  itg2addnclem2  38782  cnres2  38889  sstotbnd2  38900  sstotbnd  38901  prdstotbnd  38920  heibor1lem  38935  igenval2  39192  lshpnelb  40233  lcvexchlem4  40286  lsatexch  40292  l1cvat  40304  lkrscss  40347  lkrss  40417  lkreqN  40419  paddunN  41176  osumcllem2N  41206  pmapojoinN  41217  pl42lem2N  41229  dibglbN  42415  diblss  42419  dicvaddcl  42439  dicvscacl  42440  diclss  42442  cdlemn5pre  42449  dihord5apre  42511  dihglblem3N  42544  dihglb2  42591  dochsat  42632  dochshpncl  42633  djhspss  42655  dihsumssj  42657  mapdlsm  42913  hdmaprnlem3eN  43107  hdmaplkr  43162  lnmlsslnm  44276  lmhmfgima  44279  hbtlem6  44323  omabs2  44526  tfsconcatrev  44542  naddwordnexlem0  44590  trrelsuperreldg  44860  iunrelexpuztr  44911  clsk1indlem2  45234  grumnudlem  45461  dvsconst  45506  dvsinax  47128  dvbdfbdioolem1  47143  itgsinexplem1  47169  itgperiod  47196  stoweidlem39  47254  dirkeritg  47317  fourierdlem48  47369  fourierdlem49  47370  fourierdlem70  47391  fourierdlem71  47392  fourierdlem81  47402  issalgend  47553  chnsubseqwl  48094  tmachlem-agreeprod  48152  f1oresf1o  48565  clnbgrgrim  49237  rmsuppss  49687  restcls2lem  50232  iscnrm3rlem7  50265