Theorem sseqtrri 3983

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 3982	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3901

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 2708

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

This theorem is referenced by:  3sstr4i  3985  eqimss2i  3995  difsssymdif  4215  snsspr1  4770  snsspr2  4771  snsstp1  4772  snsstp2  4773  snsstp3  4774  unissint  4927  iunxdif2  5009  pwpwssunieq  5059  intabs  5294  inxpssres  5641  elopaelxp  5714  opabssxp  5716  dmresi  6011  cnvimass  6041  sofld  6145  cnvcnv  6150  cnvssrndm  6229  sssucid  6399  f1imadifssran  6578  cnvimainrn  7012  fvclss  7187  dmmpossx  8010  suppun  8126  frrlem12  8239  tfrlem11  8319  oawordeulem  8481  mapexOLD  8769  trcl  9637  djuunxp  9833  dfac3  10031  cfsuc  10167  isfin4p1  10225  fin23lem11  10227  domtriomlem  10352  ttukeylem1  10419  ttukeylem7  10425  brdom7disj  10441  brdom6disj  10442  fingch  10534  fpwwe2lem12  10553  canthp1lem2  10564  wunex2  10649  wunex3  10652  ressxr  11176  ltrelxr  11193  nnssnn0  12404  un0addcl  12434  un0mulcl  12435  nn0ssxnn0  12477  caubnd  15282  isumclim3  15682  iprodclim3  15923  bpoly4  15982  fprodefsum  16018  znnen  16137  isprm3  16610  phimullem  16706  isstruct2  17076  2strbas  17155  rngbase  17219  rngplusg  17220  rngmulr  17221  srngbase  17230  srngplusg  17231  srngmulr  17232  srnginvl  17233  lmodbase  17246  lmodplusg  17247  lmodsca  17248  lmodvsca  17249  ipsbase  17257  ipsaddg  17258  ipsmulr  17259  ipssca  17260  ipsvsca  17261  ipsip  17262  phlbase  17267  phlplusg  17268  phlsca  17269  phlvsca  17270  phlip  17271  topgrpbas  17282  topgrpplusg  17283  topgrptset  17284  otpsbas  17297  otpstset  17298  otpsle  17299  odrngbas  17324  odrngplusg  17325  odrngmulr  17326  odrngtset  17327  odrngle  17328  odrngds  17329  homarw  17970  ipoval  18453  ipolerval  18455  eqgfval  19105  cycsubg  19137  symgbas  19301  symgsubmefmndALT  19332  islbs3  21110  cnfldbas  21313  mpocnfldadd  21314  mpocnfldmul  21316  cnfldcj  21318  cnfldtset  21319  cnfldle  21320  cnfldds  21321  cnfldunif  21322  cnfldbasOLD  21328  cnfldaddOLD  21329  cnfldmulOLD  21330  cnfldcjOLD  21331  cnfldtsetOLD  21332  cnfldleOLD  21333  cnflddsOLD  21334  cnfldunifOLD  21335  basdif0  22897  iscldtop  23039  iocpnfordt  23159  icomnfordt  23160  iooordt  23161  cnrest2  23230  cmpcov2  23334  fiuncmp  23348  bwth  23354  indisconn  23362  locfincmp  23470  xkococnlem  23603  hmphdis  23740  uzrest  23841  ufildr  23875  fin1aufil  23876  eltsms  24077  ustval  24147  qtopbaslem  24702  tgqioo  24744  re2ndc  24745  xrhmeo  24900  bndth  24913  pi1xfrcnvlem  25012  ovolficcss  25426  nulmbl2  25493  uniiccdif  25535  opnmbllem  25558  opnmblALT  25560  mbfimaopnlem  25612  i1fima  25635  i1fima2  25636  i1fd  25638  c1liplem1  25957  deg1n0ima  26050  efcvx  26415  dvrelog  26602  dvloglem  26613  logf1o2  26615  dvlog  26616  ressatans  26900  wilthlem3  27036  bday1  27810  negsproplem2  28025  negbdaylem  28052  oncutlt  28260  oniso  28267  bdayons  28272  bdayn0p1  28365  trkgbas  28517  trkgdist  28518  trkgitv  28519  ex-ss  30502  ajfval  30884  ipasslem8  30912  hlimcaui  31311  shsspwh  31321  hhssabloi  31337  hhssnv  31339  hhshsslem1  31342  shunssji  31444  sshhococi  31621  pjoml6i  31664  osumcori  31718  mayete3i  31803  mayetes3i  31804  imaelshi  32133  pjclem1  32270  pjci  32275  mdcompli  32504  dmdcompli  32505  xppreima  32723  gsummpt2co  33131  cycpmrn  33225  elrgspnsubrunlem2  33330  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  circtopn  33994  esumpcvgval  34235  esumcvg  34243  ldgenpisyslem3  34322  elmbfmvol2  34424  sxbrsigalem0  34428  eulerpartlemsv3  34518  ballotlem7  34693  rpsqrtcn  34750  bnj931  34926  bnj1137  35151  fineqvnttrclse  35280  subfacp1lem2a  35374  subfacp1lem2b  35375  erdszelem2  35386  kur14lem7  35406  kur14lem9  35408  dfon2lem2  35976  regsfromunir1  36670  bj-snglsstag  37182  bj-2upln1upl  37225  bj-0int  37302  bj-opabssvv  37351  bj-ccssccbar  37418  bj-ccinftyssccbar  37419  bj-rvecsscvec  37505  icoreelrn  37562  finxpreclem3  37594  imadifss  37792  poimirlem4  37821  poimirlem26  37843  poimirlem27  37844  opnmbllem0  37853  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  volsupnfl  37862  sdclem2  37939  heibor1lem  38006  refrelsredund4  38885  dicval  41432  dvhdimlem  41700  ismrc  42939  mapfzcons1cl  42956  2rexfrabdioph  43034  3rexfrabdioph  43035  4rexfrabdioph  43036  6rexfrabdioph  43037  7rexfrabdioph  43038  rabdiophlem2  43040  jm2.27dlem5  43251  algbase  43412  algaddg  43413  algmulr  43414  algsca  43415  algvsca  43416  intimass2  43892  comptiunov2i  43943  relexp0a  43953  lhe4.4ex1a  44566  iocnct  45782  iccnct  45783  dvcosre  46152  fourierdlem46  46392  fourierdlem57  46403  fourierdlem58  46404  fourierdlem62  46408  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem114  46460  sge0split  46649  sge0uzfsumgt  46684  hoiprodp1  46828  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  sbgoldbo  48029  usgrexmpl1lem  48263  usgrexmpl2lem  48268  dmmpossx2  48579  ipoglb0  49235  mreclat  49238  catbas  49467  cathomfval  49468  catcofval  49469  aacllem  50042