Theorem sseqtrrd 3945

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  3sstr4d  3963  fssrescdmd  7127  funfvima2d  7238  fnfvima  7239  frrlem8  8314  frrlem10  8316  fprresex  8331  oaordi  8557  omordi  8577  omlimcl  8589  oen0  8598  domunsncan  9099  f1opwfi  9348  cantnfle  9675  cantnflt  9676  cantnflem1d  9692  ttrcltr  9720  r1pwss  9794  rankxplim3  9901  acndom2  10136  fodomfi2  10142  cflm  10330  cflim2  10344  isf34lem5  10459  isf34lem7  10460  isf34lem6  10461  axdc2lem  10529  ttukeylem5  10594  wunex2  10826  ssfzunsn  13707  ccatass  14737  swrdval2  14798  splfv2a  14909  revccat  14919  cshimadifsn  14984  cshimadifsn0  14985  rtrclreclem1  15215  rtrclreclem2  15217  sumrblem  15882  prodrblem  16101  dfphi2  16956  vdwlem1  17164  basprssdmsets  17404  imasaddfnlem  17705  imasaddvallem  17706  imasvscafn  17714  imasvscaval  17715  mreexexlem4d  17826  mreexfidimd  17829  sscpwex  17995  acsmap2d  18734  gsumress  18876  subsubmgm  18904  subsubm  19017  frmdsssubm  19062  frmdss2  19064  subsubg  19365  cntzmhm2  19561  cntzcmnf  20064  ablcntzd  20076  gsumzsubmcl  20137  gsumconst  20153  gsumzmhm  20156  subgdmdprd  20255  dprdcntz2  20259  dprd2da  20263  dmdprdsplit2lem  20266  ablfac1eu  20294  pgpfaclem1  20302  pgpfaclem2  20303  subsubrng  20820  subsubrg  20855  issubdrg  21042  subdrgint  21065  lmhmlsp  21329  lspsntri  21377  lspindpi  21415  rspprop  21529  lidldvgen  21663  gsumfsum  21745  mrccss  22005  frlmsslsp  22107  lindsdom  22161  opsrtoslem2  22370  ressply1evl  22693  scmatsgrp1  22842  toponss  23250  ssntr  23381  elcls3  23406  toponmre  23416  neiptoptop  23454  neiptopnei  23455  neitr  23503  ordtbas  23515  ordtopn1  23517  ordtopn2  23518  iscnp3  23567  tgcn  23575  tgcnp  23576  ssidcn  23578  cnclsi  23595  cncls  23597  cncnp  23603  lmcld  23626  tgcmp  23724  cnconn  23745  connima  23748  clsconn  23753  conncompcld  23757  1stccnp  23786  kgentopon  23862  llycmpkgen2  23874  1stckgen  23878  kgencn2  23881  ptopn  23907  txcls  23928  ptpjcn  23935  ptclsg  23939  xkoccn  23943  txcnp  23944  ptcnplem  23945  txcmplem2  23966  xkoptsub  23978  xkopt  23979  xkoco2cn  23982  xkococnlem  23983  xkoinjcn  24011  imasnopn  24014  imasncld  24015  imasncls  24016  qtopkgen  24034  basqtop  24035  tgqtop  24036  qtoprest  24041  kqsat  24055  kqcldsat  24057  kqnrmlem1  24067  kqnrmlem2  24068  hmeontr  24093  reghmph  24117  nrmhmph  24118  fmfnfmlem4  24281  fmfnfm  24282  flimopn  24299  flimclslem  24308  flfnei  24315  lmflf  24329  txflf  24330  fclsopn  24338  fclsfnflim  24351  alexsublem  24368  ptcmplem3  24378  cnextcn  24391  efmndtmd  24425  submtmd  24428  subgtgp  24429  symgtgp  24430  clssubg  24433  clsnsg  24434  tgpconncompeqg  24436  snclseqg  24440  tsmscls  24462  trust  24553  restutop  24561  restutopopn  24562  utop3cls  24575  utopreg  24576  trcfilu  24617  blssec  24759  prdsbl  24815  blssopn  24819  metcnp  24865  cfilucfil  24883  psmetutop  24891  iccntr  25146  icccmplem2  25148  reconnlem1  25151  metnrmlem1a  25183  metnrmlem1  25184  metnrmlem2  25185  metnrmlem3  25186  cnheibor  25281  lebnumlem1  25287  lebnumlem3  25289  lebnumii  25292  clsocv  25576  iscfil2  25592  iscmet3  25619  cmetss  25642  relcmpcmet  25644  bcthlem5  25654  itg1addlem5  26026  perfdvf  26228  dvres3  26238  dvres3a  26239  dvcmul  26269  dvcmulf  26270  dvlip2  26320  lhop1lem  26338  dvcnvrelem1  26342  dvcnvrelem2  26343  dvcnvre  26344  dvcvx  26345  plyco0  26515  plyaddlem1  26537  plymullem1  26538  aalioulem3  26666  ulmdvlem1  26732  precsexlem6  28603  precsexlem7  28604  bdayn0p1  28760  bdaypw2n0bndlem  28854  z12bdaylem2  28862  plngrotlem1  29270  lnssplnglem  29274  prlngpln4  29441  quadcgrprlng  29449  axcontlem10  29556  eengtrkg  29569  wlkp1lem7  30263  revwlk  30272  cyclnumvtx  30393  1wlkdlem4  30736  hsupunss  31950  pjpjpre  32026  ssmd2  32919  superpos  32961  atexch  32988  curry2ima  33349  pfxf1  33555  gsumhashmul  33674  symgcom2  33691  pmtrcnelor  33698  cycpmco2lem7  33739  cycpmconjvlem  33748  cycpmconjv  33749  cyc3conja  33764  elrgspnsubrunlem2  33855  subsdrg  33906  nsgmgc  34009  nsgqusf1olem3  34012  elrspunidl  34024  mxidlprm  34041  rprmdvdsprod  34112  dfufd2lem  34127  esplyfvaln  34252  lssdimle  34286  dimkerim  34305  fedgmullem1  34307  fedgmullem2  34308  fedgmul  34309  dimlssid  34310  fldsdrgfldext2  34340  fldextrspunlsplem  34351  fldextrspunlsp  34352  fldextrspunlem1  34353  fldextrspundgdvdslem  34358  fldextrspundgdvds  34359  constr01  34420  constrmon  34422  constrextdg2lem  34426  constrext2chnlem  34428  madjusmdetlem2  34506  zarclsun  34548  rhmpreimacnlem  34562  ordtconnlem1  34602  measiuns  34896  imambfm  34940  cnmbfm  34941  dya2iocnrect  34959  omsfval  34972  omssubaddlem  34977  omssubadd  34978  totprobd  35104  fzssfzo  35217  signstfvn  35244  bnj999  35634  bnj1408  35712  bnj1442  35725  bnj1450  35726  bnj1501  35743  fnrelpredd  35772  cvmsss2  36125  cvmliftmolem1  36132  cvmliftlem3  36138  cvmlift2lem9  36162  cvmlift2lem11  36164  cvmlift3lem6  36175  cvmlift3lem7  36176  ssmclslem  36416  mclsax  36420  mclsppslem  36434  mclspps  36435  dfrdg2  36649  neiin  37212  neibastop2  37241  filnetlem4  37261  weiunfrlem  37344  rdgssun  38394  poimirlem11  38642  poimirlem12  38643  itg2addnclem2  38683  cnres2  38790  sstotbnd2  38801  sstotbnd  38802  prdstotbnd  38821  heibor1lem  38836  igenval2  39093  lshpnelb  40134  lcvexchlem4  40187  lsatexch  40193  l1cvat  40205  lkrscss  40248  lkrss  40318  lkreqN  40320  paddunN  41077  osumcllem2N  41107  pmapojoinN  41118  pl42lem2N  41130  dibglbN  42316  diblss  42320  dicvaddcl  42340  dicvscacl  42341  diclss  42343  cdlemn5pre  42350  dihord5apre  42412  dihglblem3N  42445  dihglb2  42492  dochsat  42533  dochshpncl  42534  djhspss  42556  dihsumssj  42558  mapdlsm  42814  hdmaprnlem3eN  43008  hdmaplkr  43063  lnmlsslnm  44176  lmhmfgima  44179  hbtlem6  44224  omabs2  44427  tfsconcatrev  44443  naddwordnexlem0  44491  trrelsuperreldg  44761  iunrelexpuztr  44812  clsk1indlem2  45135  grumnudlem  45362  dvsconst  45407  dvsinax  47016  dvbdfbdioolem1  47031  itgsinexplem1  47057  itgperiod  47084  stoweidlem39  47142  dirkeritg  47205  fourierdlem48  47257  fourierdlem49  47258  fourierdlem70  47279  fourierdlem71  47280  fourierdlem81  47290  issalgend  47441  chnsubseqwl  47982  tmachlem-agreeprod  48040  f1oresf1o  48453  clnbgrgrim  49125  rmsuppss  49575  restcls2lem  50120  iscnrm3rlem7  50153