Theorem sseqtrri 3971

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)

Hypotheses

Ref	Expression
sseqtrri.1	⊢ 𝐴 ⊆ 𝐵
sseqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
sseqtrri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtrri

Step	Hyp	Ref	Expression
1		sseqtrri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2745	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 3970	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  3sstr4i  3973  eqimss2i  3983  difsssymdif  4203  snsspr1  4757  snsspr2  4758  snsstp1  4759  snsstp2  4760  snsstp3  4761  unissint  4914  iunxdif2  4996  pwpwssunieq  5046  intabs  5290  inxpssres  5648  elopaelxp  5721  opabssxp  5723  dmresi  6017  cnvimass  6047  sofld  6151  cnvcnv  6156  cnvssrndm  6235  sssucid  6405  f1imadifssran  6584  cnvimainrn  7019  fvclss  7196  dmmpossx  8019  suppun  8134  frrlem12  8247  tfrlem11  8327  oawordeulem  8489  mapexOLD  8779  trcl  9649  djuunxp  9845  dfac3  10043  cfsuc  10179  isfin4p1  10237  fin23lem11  10239  domtriomlem  10364  ttukeylem1  10431  ttukeylem7  10437  brdom7disj  10453  brdom6disj  10454  fingch  10546  fpwwe2lem12  10565  canthp1lem2  10576  wunex2  10661  wunex3  10664  ressxr  11189  ltrelxr  11206  nnssnn0  12440  un0addcl  12470  un0mulcl  12471  nn0ssxnn0  12513  caubnd  15321  isumclim3  15721  iprodclim3  15965  bpoly4  16024  fprodefsum  16060  znnen  16179  isprm3  16652  phimullem  16749  isstruct2  17119  2strbas  17198  rngbase  17262  rngplusg  17263  rngmulr  17264  srngbase  17273  srngplusg  17274  srngmulr  17275  srnginvl  17276  lmodbase  17289  lmodplusg  17290  lmodsca  17291  lmodvsca  17292  ipsbase  17300  ipsaddg  17301  ipsmulr  17302  ipssca  17303  ipsvsca  17304  ipsip  17305  phlbase  17310  phlplusg  17311  phlsca  17312  phlvsca  17313  phlip  17314  topgrpbas  17325  topgrpplusg  17326  topgrptset  17327  otpsbas  17340  otpstset  17341  otpsle  17342  odrngbas  17367  odrngplusg  17368  odrngmulr  17369  odrngtset  17370  odrngle  17371  odrngds  17372  homarw  18013  ipoval  18496  ipolerval  18498  eqgfval  19151  cycsubg  19183  symgbas  19347  symgsubmefmndALT  19378  islbs3  21153  cnfldbas  21356  mpocnfldadd  21357  mpocnfldmul  21359  cnfldcj  21361  cnfldtset  21362  cnfldle  21363  cnfldds  21364  cnfldunif  21365  basdif0  22918  iscldtop  23060  iocpnfordt  23180  icomnfordt  23181  iooordt  23182  cnrest2  23251  cmpcov2  23355  fiuncmp  23369  bwth  23375  indisconn  23383  locfincmp  23491  xkococnlem  23624  hmphdis  23761  uzrest  23862  ufildr  23896  fin1aufil  23897  eltsms  24098  ustval  24168  qtopbaslem  24723  tgqioo  24765  re2ndc  24766  xrhmeo  24913  bndth  24925  pi1xfrcnvlem  25023  ovolficcss  25436  nulmbl2  25503  uniiccdif  25545  opnmbllem  25568  opnmblALT  25570  mbfimaopnlem  25622  i1fima  25645  i1fima2  25646  i1fd  25648  c1liplem1  25963  deg1n0ima  26054  efcvx  26414  dvrelog  26601  dvloglem  26612  logf1o2  26614  dvlog  26615  ressatans  26898  wilthlem3  27033  bday1  27806  negsproplem2  28021  negbdaylem  28048  oncutlt  28256  oniso  28263  bdayons  28268  bdayn0p1  28361  trkgbas  28513  trkgdist  28514  trkgitv  28515  ex-ss  30497  ajfval  30880  ipasslem8  30908  hlimcaui  31307  shsspwh  31317  hhssabloi  31333  hhssnv  31335  hhshsslem1  31338  shunssji  31440  sshhococi  31617  pjoml6i  31660  osumcori  31714  mayete3i  31799  mayetes3i  31800  imaelshi  32129  pjclem1  32266  pjci  32271  mdcompli  32500  dmdcompli  32501  xppreima  32718  gsummpt2co  33109  cycpmrn  33204  elrgspnsubrunlem2  33309  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  circtopn  33981  esumpcvgval  34222  esumcvg  34230  ldgenpisyslem3  34309  elmbfmvol2  34411  sxbrsigalem0  34415  eulerpartlemsv3  34505  ballotlem7  34680  rpsqrtcn  34737  bnj931  34913  bnj1137  35137  fineqvnttrclse  35268  subfacp1lem2a  35362  subfacp1lem2b  35363  erdszelem2  35374  kur14lem7  35394  kur14lem9  35396  dfon2lem2  35964  regsfromunir1  36722  bj-snglsstag  37288  bj-2upln1upl  37331  bj-0int  37413  bj-opabssvv  37464  bj-ccssccbar  37531  bj-ccinftyssccbar  37532  bj-rvecsscvec  37618  icoreelrn  37677  finxpreclem3  37709  imadifss  37916  poimirlem4  37945  poimirlem26  37967  poimirlem27  37968  opnmbllem0  37977  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  volsupnfl  37986  sdclem2  38063  heibor1lem  38130  refrelsredund4  39037  dicval  41622  dvhdimlem  41890  ismrc  43133  mapfzcons1cl  43150  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  rabdiophlem2  43230  jm2.27dlem5  43441  algbase  43602  algaddg  43603  algmulr  43604  algsca  43605  algvsca  43606  intimass2  44082  comptiunov2i  44133  relexp0a  44143  lhe4.4ex1a  44756  iocnct  45970  iccnct  45971  dvcosre  46340  fourierdlem46  46580  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  sge0split  46837  sge0uzfsumgt  46872  hoiprodp1  47016  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  sbgoldbo  48263  usgrexmpl1lem  48497  usgrexmpl2lem  48502  dmmpossx2  48813  ipoglb0  49469  mreclat  49472  catbas  49701  cathomfval  49702  catcofval  49703  aacllem  50276