Theorem sseqtrri 4032

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 2743	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 4031	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqimss2i  4056  difsssymdif  4268  snsspr1  4818  snsspr2  4819  snsstp1  4820  snsstp2  4821  snsstp3  4822  unissint  4976  iunxdif2  5057  pwpwssunieq  5108  intabs  5354  inxpssres  5705  elopaelxp  5777  opabssxp  5780  dmresi  6071  cnvimass  6101  sofld  6208  cnvcnv  6213  cnvssrndm  6292  sssucid  6465  cnvimainrn  7086  fvclss  7260  dmmpossx  8089  suppun  8207  frrlem12  8320  wfrlem14OLD  8360  tfrlem11  8426  oawordeulem  8590  mapexOLD  8870  trcl  9765  djuunxp  9958  dfac3  10158  cfsuc  10294  isfin4p1  10352  fin23lem11  10354  domtriomlem  10479  ttukeylem1  10546  ttukeylem7  10552  brdom7disj  10568  brdom6disj  10569  fingch  10660  fpwwe2lem12  10679  canthp1lem2  10690  wunex2  10775  wunex3  10778  ressxr  11302  ltrelxr  11319  nnssnn0  12526  un0addcl  12556  un0mulcl  12557  nn0ssxnn0  12599  caubnd  15393  isumclim3  15791  iprodclim3  16032  bpoly4  16091  fprodefsum  16127  znnen  16244  isprm3  16716  phimullem  16812  isstruct2  17182  2strbas  17267  2strop  17268  2strbas1  17271  rngbase  17344  rngplusg  17345  rngmulr  17346  srngbase  17355  srngplusg  17356  srngmulr  17357  srnginvl  17358  lmodbase  17371  lmodplusg  17372  lmodsca  17373  lmodvsca  17374  ipsbase  17382  ipsaddg  17383  ipsmulr  17384  ipssca  17385  ipsvsca  17386  ipsip  17387  phlbase  17392  phlplusg  17393  phlsca  17394  phlvsca  17395  phlip  17396  topgrpbas  17407  topgrpplusg  17408  topgrptset  17409  otpsbas  17422  otpstset  17423  otpsle  17424  odrngbas  17449  odrngplusg  17450  odrngmulr  17451  odrngtset  17452  odrngle  17453  odrngds  17454  homarw  18099  ipoval  18587  ipolerval  18589  eqgfval  19206  cycsubg  19238  symgbas  19403  symgsubmefmndALT  19435  islbs3  21174  cnfldbas  21385  mpocnfldadd  21386  mpocnfldmul  21388  cnfldcj  21390  cnfldtset  21391  cnfldle  21392  cnfldds  21393  cnfldunif  21394  cnfldbasOLD  21400  cnfldaddOLD  21401  cnfldmulOLD  21402  cnfldcjOLD  21403  cnfldtsetOLD  21404  cnfldleOLD  21405  cnflddsOLD  21406  cnfldunifOLD  21407  basdif0  22975  iscldtop  23118  iocpnfordt  23238  icomnfordt  23239  iooordt  23240  cnrest2  23309  cmpcov2  23413  fiuncmp  23427  bwth  23433  indisconn  23441  locfincmp  23549  xkococnlem  23682  hmphdis  23819  uzrest  23920  ufildr  23954  fin1aufil  23955  eltsms  24156  ustval  24226  qtopbaslem  24794  tgqioo  24835  re2ndc  24836  xrhmeo  24990  bndth  25003  pi1xfrcnvlem  25102  ovolficcss  25517  nulmbl2  25584  uniiccdif  25626  opnmbllem  25649  opnmblALT  25651  mbfimaopnlem  25703  i1fima  25726  i1fima2  25727  i1fd  25729  c1liplem1  26049  deg1n0ima  26142  efcvx  26507  dvrelog  26693  dvloglem  26704  logf1o2  26706  dvlog  26707  ressatans  26991  wilthlem3  27127  bday1s  27890  negsproplem2  28075  negsbdaylem  28102  trkgbas  28467  trkgdist  28468  trkgitv  28469  ex-ss  30455  ajfval  30837  ipasslem8  30865  hlimcaui  31264  shsspwh  31274  hhssabloi  31290  hhssnv  31292  hhshsslem1  31295  shunssji  31397  sshhococi  31574  pjoml6i  31617  osumcori  31671  mayete3i  31756  mayetes3i  31757  imaelshi  32086  pjclem1  32223  pjci  32228  mdcompli  32457  dmdcompli  32458  xppreima  32661  gsummpt2co  33033  cycpmrn  33145  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  circtopn  33797  esumpcvgval  34058  esumcvg  34066  ldgenpisyslem3  34145  elmbfmvol2  34248  sxbrsigalem0  34252  eulerpartlemsv3  34342  ballotlem7  34516  rpsqrtcn  34586  bnj931  34762  bnj1137  34987  subfacp1lem2a  35164  subfacp1lem2b  35165  erdszelem2  35176  kur14lem7  35196  kur14lem9  35198  dfon2lem2  35765  bj-snglsstag  36963  bj-2upln1upl  37006  bj-0int  37083  bj-opabssvv  37132  bj-ccssccbar  37199  bj-ccinftyssccbar  37200  bj-rvecsscvec  37286  icoreelrn  37343  finxpreclem3  37375  imadifss  37581  poimirlem4  37610  poimirlem26  37632  poimirlem27  37633  opnmbllem0  37642  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  volsupnfl  37651  sdclem2  37728  heibor1lem  37795  refrelsredund4  38613  dicval  41158  dvhdimlem  41426  ismrc  42688  mapfzcons1cl  42705  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  rabdiophlem2  42789  jm2.27dlem5  43001  algbase  43162  algaddg  43163  algmulr  43164  algsca  43165  algvsca  43166  intimass2  43644  comptiunov2i  43695  relexp0a  43705  lhe4.4ex1a  44324  iocnct  45492  iccnct  45493  dvcosre  45867  fourierdlem46  46107  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  sge0split  46364  sge0uzfsumgt  46399  hoiprodp1  46543  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  sbgoldbo  47711  usgrexmpl1lem  47915  usgrexmpl2lem  47920  dmmpossx2  48181  ipoglb0  48782  mreclat  48785  aacllem  49031