Theorem sseqtrrd 3996

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  3sstr4d  4014  fssrescdmd  7115  funfvima2d  7223  fnfvima  7224  frrlem8  8290  frrlem10  8292  fprresex  8307  wfrlem17OLD  8337  oaordi  8556  omordi  8576  omlimcl  8588  oen0  8596  domunsncan  9084  f1opwfi  9366  cantnfle  9683  cantnflt  9684  cantnflem1d  9700  ttrcltr  9728  r1pwss  9796  rankxplim3  9893  acndom2  10066  fodomfi2  10072  cflm  10262  cflim2  10275  isf34lem5  10390  isf34lem7  10391  isf34lem6  10392  axdc2lem  10460  ttukeylem5  10525  wunex2  10750  ssfzunsn  13585  ccatass  14604  swrdval2  14662  splfv2a  14772  revccat  14782  cshimadifsn  14846  cshimadifsn0  14847  rtrclreclem1  15074  rtrclreclem2  15076  sumrblem  15725  prodrblem  15943  dfphi2  16791  vdwlem1  16999  basprssdmsets  17238  imasaddfnlem  17540  imasaddvallem  17541  imasvscafn  17549  imasvscaval  17550  mreexexlem4d  17657  mreexfidimd  17660  sscpwex  17826  acsmap2d  18563  gsumress  18658  subsubmgm  18686  subsubm  18792  frmdsssubm  18837  frmdss2  18839  subsubg  19130  cntzmhm2  19323  cntzcmnf  19824  ablcntzd  19836  gsumzsubmcl  19897  gsumconst  19913  gsumzmhm  19916  subgdmdprd  20015  dprdcntz2  20019  dprd2da  20023  dmdprdsplit2lem  20026  ablfac1eu  20054  pgpfaclem1  20062  pgpfaclem2  20063  subsubrng  20521  subsubrg  20556  issubdrg  20738  subdrgint  20761  lmhmlsp  21005  lspsntri  21053  lspindpi  21091  lidldvgen  21293  gsumfsum  21400  mrccss  21652  frlmsslsp  21754  opsrtoslem2  22012  ressply1evl  22306  scmatsgrp1  22458  toponss  22863  ssntr  22994  elcls3  23019  toponmre  23029  neiptoptop  23067  neiptopnei  23068  neitr  23116  ordtbas  23128  ordtopn1  23130  ordtopn2  23131  iscnp3  23180  tgcn  23188  tgcnp  23189  ssidcn  23191  cnclsi  23208  cncls  23210  cncnp  23216  lmcld  23239  tgcmp  23337  cnconn  23358  connima  23361  clsconn  23366  conncompcld  23370  1stccnp  23398  kgentopon  23474  llycmpkgen2  23486  1stckgen  23490  kgencn2  23493  ptopn  23519  txcls  23540  ptpjcn  23547  ptclsg  23551  xkoccn  23555  txcnp  23556  ptcnplem  23557  txcmplem2  23578  xkoptsub  23590  xkopt  23591  xkoco2cn  23594  xkococnlem  23595  xkoinjcn  23623  imasnopn  23626  imasncld  23627  imasncls  23628  qtopkgen  23646  basqtop  23647  tgqtop  23648  qtoprest  23653  kqsat  23667  kqcldsat  23669  kqnrmlem1  23679  kqnrmlem2  23680  hmeontr  23705  reghmph  23729  nrmhmph  23730  fmfnfmlem4  23893  fmfnfm  23894  flimopn  23911  flimclslem  23920  flfnei  23927  lmflf  23941  txflf  23942  fclsopn  23950  fclsfnflim  23963  alexsublem  23980  ptcmplem3  23990  cnextcn  24003  efmndtmd  24037  submtmd  24040  subgtgp  24041  symgtgp  24042  clssubg  24045  clsnsg  24046  tgpconncompeqg  24048  snclseqg  24052  tsmscls  24074  trust  24166  restutop  24174  restutopopn  24175  utop3cls  24188  utopreg  24189  trcfilu  24230  blssec  24372  prdsbl  24428  blssopn  24432  metcnp  24478  cfilucfil  24496  psmetutop  24504  iccntr  24759  icccmplem2  24761  reconnlem1  24764  metnrmlem1a  24796  metnrmlem1  24797  metnrmlem2  24798  metnrmlem3  24799  cnheibor  24903  lebnumlem1  24909  lebnumlem3  24911  lebnumii  24914  clsocv  25200  iscfil2  25216  iscmet3  25243  cmetss  25266  relcmpcmet  25268  bcthlem5  25278  itg1addlem5  25651  perfdvf  25854  dvres3  25864  dvres3a  25865  dvcmul  25897  dvcmulf  25898  dvlip2  25950  lhop1lem  25968  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvcvx  25975  plyco0  26147  plyaddlem1  26168  plymullem1  26169  aalioulem3  26292  ulmdvlem1  26359  precsexlem6  28153  precsexlem7  28154  axcontlem10  28898  eengtrkg  28911  wlkp1lem7  29605  cyclnumvtx  29728  1wlkdlem4  30067  hsupunss  31270  pjpjpre  31346  ssmd2  32239  superpos  32281  atexch  32308  curry2ima  32632  pfxf1  32863  gsumhashmul  33001  symgcom2  33041  pmtrcnelor  33048  cycpmco2lem7  33089  cycpmconjvlem  33098  cycpmconjv  33099  cyc3conja  33114  elrgspnsubrunlem2  33189  subsdrg  33238  nsgmgc  33373  nsgqusf1olem3  33376  elrspunidl  33389  mxidlprm  33431  rprmdvdsprod  33495  dfufd2lem  33510  lssdimle  33593  dimkerim  33613  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  dimlssid  33618  fldsdrgfldext2  33650  fldextrspunlsplem  33660  fldextrspunlsp  33661  fldextrspunlem1  33662  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  constr01  33722  constrmon  33724  constrextdg2lem  33728  constrext2chnlem  33730  madjusmdetlem2  33805  zarclsun  33847  rhmpreimacnlem  33861  ordtconnlem1  33901  measiuns  34194  imambfm  34240  cnmbfm  34241  dya2iocnrect  34259  omsfval  34272  omssubaddlem  34277  omssubadd  34278  totprobd  34404  fzssfzo  34517  signstfvn  34547  bnj999  34935  bnj1408  35013  bnj1442  35026  bnj1450  35027  bnj1501  35044  fnrelpredd  35066  revwlk  35093  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  36296  neibastop2  36325  filnetlem4  36345  weiunfrlem  36428  rdgssun  37342  lindsdom  37584  poimirlem11  37601  poimirlem12  37602  itg2addnclem2  37642  cnres2  37733  sstotbnd2  37744  sstotbnd  37745  prdstotbnd  37764  heibor1lem  37779  igenval2  38036  lshpnelb  38948  lcvexchlem4  39001  lsatexch  39007  l1cvat  39019  lkrscss  39062  lkrss  39132  lkreqN  39134  paddunN  39892  osumcllem2N  39922  pmapojoinN  39933  pl42lem2N  39945  dibglbN  41131  diblss  41135  dicvaddcl  41155  dicvscacl  41156  diclss  41158  cdlemn5pre  41165  dihord5apre  41227  dihglblem3N  41260  dihglb2  41307  dochsat  41348  dochshpncl  41349  djhspss  41371  dihsumssj  41373  mapdlsm  41629  hdmaprnlem3eN  41823  hdmaplkr  41878  fnwe2lem2  43022  lnmlsslnm  43052  lmhmfgima  43055  hbtlem6  43100  omabs2  43303  tfsconcatrev  43319  naddwordnexlem0  43367  trrelsuperreldg  43639  iunrelexpuztr  43690  clsk1indlem2  44013  grumnudlem  44257  dvsconst  44302  dvsinax  45890  dvbdfbdioolem1  45905  itgsinexplem1  45931  itgperiod  45958  stoweidlem39  46016  dirkeritg  46079  fourierdlem48  46131  fourierdlem49  46132  fourierdlem70  46153  fourierdlem71  46154  fourierdlem81  46164  issalgend  46315  f1oresf1o  47267  clnbgrgrim  47895  rmsuppss  48293  restcls2lem  48835  iscnrm3rlem7  48868