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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  3sstr4d  3986  fssrescdmd  7065  funfvima2d  7172  fnfvima  7173  frrlem8  8229  frrlem10  8231  fprresex  8246  oaordi  8467  omordi  8487  omlimcl  8499  oen0  8507  domunsncan  8997  f1opwfi  9247  cantnfle  9568  cantnflt  9569  cantnflem1d  9585  ttrcltr  9613  r1pwss  9684  rankxplim3  9781  acndom2  9952  fodomfi2  9958  cflm  10148  cflim2  10161  isf34lem5  10276  isf34lem7  10277  isf34lem6  10278  axdc2lem  10346  ttukeylem5  10411  wunex2  10636  ssfzunsn  13472  ccatass  14498  swrdval2  14556  splfv2a  14665  revccat  14675  cshimadifsn  14738  cshimadifsn0  14739  rtrclreclem1  14966  rtrclreclem2  14968  sumrblem  15620  prodrblem  15838  dfphi2  16687  vdwlem1  16895  basprssdmsets  17134  imasaddfnlem  17434  imasaddvallem  17435  imasvscafn  17443  imasvscaval  17444  mreexexlem4d  17555  mreexfidimd  17558  sscpwex  17724  acsmap2d  18463  gsumress  18592  subsubmgm  18620  subsubm  18726  frmdsssubm  18771  frmdss2  18773  subsubg  19064  cntzmhm2  19256  cntzcmnf  19759  ablcntzd  19771  gsumzsubmcl  19832  gsumconst  19848  gsumzmhm  19851  subgdmdprd  19950  dprdcntz2  19954  dprd2da  19958  dmdprdsplit2lem  19961  ablfac1eu  19989  pgpfaclem1  19997  pgpfaclem2  19998  subsubrng  20480  subsubrg  20515  issubdrg  20697  subdrgint  20720  lmhmlsp  20985  lspsntri  21033  lspindpi  21071  lidldvgen  21273  gsumfsum  21373  mrccss  21633  frlmsslsp  21735  opsrtoslem2  21992  ressply1evl  22286  scmatsgrp1  22438  toponss  22843  ssntr  22974  elcls3  22999  toponmre  23009  neiptoptop  23047  neiptopnei  23048  neitr  23096  ordtbas  23108  ordtopn1  23110  ordtopn2  23111  iscnp3  23160  tgcn  23168  tgcnp  23169  ssidcn  23171  cnclsi  23188  cncls  23190  cncnp  23196  lmcld  23219  tgcmp  23317  cnconn  23338  connima  23341  clsconn  23346  conncompcld  23350  1stccnp  23378  kgentopon  23454  llycmpkgen2  23466  1stckgen  23470  kgencn2  23473  ptopn  23499  txcls  23520  ptpjcn  23527  ptclsg  23531  xkoccn  23535  txcnp  23536  ptcnplem  23537  txcmplem2  23558  xkoptsub  23570  xkopt  23571  xkoco2cn  23574  xkococnlem  23575  xkoinjcn  23603  imasnopn  23606  imasncld  23607  imasncls  23608  qtopkgen  23626  basqtop  23627  tgqtop  23628  qtoprest  23633  kqsat  23647  kqcldsat  23649  kqnrmlem1  23659  kqnrmlem2  23660  hmeontr  23685  reghmph  23709  nrmhmph  23710  fmfnfmlem4  23873  fmfnfm  23874  flimopn  23891  flimclslem  23900  flfnei  23907  lmflf  23921  txflf  23922  fclsopn  23930  fclsfnflim  23943  alexsublem  23960  ptcmplem3  23970  cnextcn  23983  efmndtmd  24017  submtmd  24020  subgtgp  24021  symgtgp  24022  clssubg  24025  clsnsg  24026  tgpconncompeqg  24028  snclseqg  24032  tsmscls  24054  trust  24145  restutop  24153  restutopopn  24154  utop3cls  24167  utopreg  24168  trcfilu  24209  blssec  24351  prdsbl  24407  blssopn  24411  metcnp  24457  cfilucfil  24475  psmetutop  24483  iccntr  24738  icccmplem2  24740  reconnlem1  24743  metnrmlem1a  24775  metnrmlem1  24776  metnrmlem2  24777  metnrmlem3  24778  cnheibor  24882  lebnumlem1  24888  lebnumlem3  24890  lebnumii  24893  clsocv  25178  iscfil2  25194  iscmet3  25221  cmetss  25244  relcmpcmet  25246  bcthlem5  25256  itg1addlem5  25629  perfdvf  25832  dvres3  25842  dvres3a  25843  dvcmul  25875  dvcmulf  25876  dvlip2  25928  lhop1lem  25946  dvcnvrelem1  25950  dvcnvrelem2  25951  dvcnvre  25952  dvcvx  25953  plyco0  26125  plyaddlem1  26146  plymullem1  26147  aalioulem3  26270  ulmdvlem1  26337  precsexlem6  28151  precsexlem7  28152  bdayn0p1  28295  axcontlem10  28953  eengtrkg  28966  wlkp1lem7  29658  cyclnumvtx  29780  1wlkdlem4  30122  hsupunss  31325  pjpjpre  31401  ssmd2  32294  superpos  32336  atexch  32363  curry2ima  32694  pfxf1  32930  gsumhashmul  33048  symgcom2  33060  pmtrcnelor  33067  cycpmco2lem7  33108  cycpmconjvlem  33117  cycpmconjv  33118  cyc3conja  33133  elrgspnsubrunlem2  33222  subsdrg  33271  nsgmgc  33384  nsgqusf1olem3  33387  elrspunidl  33400  mxidlprm  33442  rprmdvdsprod  33506  dfufd2lem  33521  lssdimle  33641  dimkerim  33661  fedgmullem1  33663  fedgmullem2  33664  fedgmul  33665  dimlssid  33666  fldsdrgfldext2  33696  fldextrspunlsplem  33707  fldextrspunlsp  33708  fldextrspunlem1  33709  fldextrspundgdvdslem  33714  fldextrspundgdvds  33715  constr01  33776  constrmon  33778  constrextdg2lem  33782  constrext2chnlem  33784  madjusmdetlem2  33862  zarclsun  33904  rhmpreimacnlem  33918  ordtconnlem1  33958  measiuns  34251  imambfm  34296  cnmbfm  34297  dya2iocnrect  34315  omsfval  34328  omssubaddlem  34333  omssubadd  34334  totprobd  34460  fzssfzo  34573  signstfvn  34603  bnj999  34991  bnj1408  35069  bnj1442  35082  bnj1450  35083  bnj1501  35100  fnrelpredd  35123  revwlk  35190  cvmsss2  35339  cvmliftmolem1  35346  cvmliftlem3  35352  cvmlift2lem9  35376  cvmlift2lem11  35378  cvmlift3lem6  35389  cvmlift3lem7  35390  ssmclslem  35630  mclsax  35634  mclsppslem  35648  mclspps  35649  dfrdg2  35858  neiin  36397  neibastop2  36426  filnetlem4  36446  weiunfrlem  36529  rdgssun  37443  lindsdom  37675  poimirlem11  37692  poimirlem12  37693  itg2addnclem2  37733  cnres2  37824  sstotbnd2  37835  sstotbnd  37836  prdstotbnd  37855  heibor1lem  37870  igenval2  38127  lshpnelb  39104  lcvexchlem4  39157  lsatexch  39163  l1cvat  39175  lkrscss  39218  lkrss  39288  lkreqN  39290  paddunN  40047  osumcllem2N  40077  pmapojoinN  40088  pl42lem2N  40100  dibglbN  41286  diblss  41290  dicvaddcl  41310  dicvscacl  41311  diclss  41313  cdlemn5pre  41320  dihord5apre  41382  dihglblem3N  41415  dihglb2  41462  dochsat  41503  dochshpncl  41504  djhspss  41526  dihsumssj  41528  mapdlsm  41784  hdmaprnlem3eN  41978  hdmaplkr  42033  fnwe2lem2  43169  lnmlsslnm  43199  lmhmfgima  43202  hbtlem6  43247  omabs2  43450  tfsconcatrev  43466  naddwordnexlem0  43514  trrelsuperreldg  43786  iunrelexpuztr  43837  clsk1indlem2  44160  grumnudlem  44403  dvsconst  44448  dvsinax  46036  dvbdfbdioolem1  46051  itgsinexplem1  46077  itgperiod  46104  stoweidlem39  46162  dirkeritg  46225  fourierdlem48  46277  fourierdlem49  46278  fourierdlem70  46299  fourierdlem71  46300  fourierdlem81  46310  issalgend  46461  chnsubseqwl  47002  f1oresf1o  47415  clnbgrgrim  48059  rmsuppss  48495  restcls2lem  49038  iscnrm3rlem7  49071