Theorem sseqtrri 3915

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

Syntax hints:   = wceq 1542   ⊆ wss 3844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-in 3851  df-ss 3861

This theorem is referenced by:  eqimss2i  3937  difsssymdif  4144  snsspr1  4703  snsspr2  4704  snsstp1  4705  snsstp2  4706  snsstp3  4707  unissint  4861  iunxdif2  4940  pwpwssunieq  4990  intabs  5211  inxpssres  5543  opabssxp  5615  dmresi  5896  cnvimass  5924  sofld  6020  cnvcnv  6025  cnvssrndm  6104  sssucid  6250  cnvimainrn  6847  fvclss  7015  dmmpossx  7792  suppun  7882  wfrlem14  8000  tfrlem11  8056  oawordeulem  8214  mapex  8446  trcl  9246  djuunxp  9426  dfac3  9624  cfsuc  9760  isfin4p1  9818  fin23lem11  9820  domtriomlem  9945  ttukeylem1  10012  ttukeylem7  10018  brdom7disj  10034  brdom6disj  10035  fingch  10126  fpwwe2lem12  10145  canthp1lem2  10156  wunex2  10241  wunex3  10244  ressxr  10766  ltrelxr  10783  nnssnn0  11982  un0addcl  12012  un0mulcl  12013  nn0ssxnn0  12054  caubnd  14811  isumclim3  15210  iprodclim3  15449  bpoly4  15508  fprodefsum  15543  znnen  15660  isprm3  16127  phimullem  16219  isstruct2  16599  2strbas  16709  2strop  16710  2strbas1  16712  rngbase  16726  rngplusg  16727  rngmulr  16728  srngbase  16734  srngplusg  16735  srngmulr  16736  srnginvl  16737  lmodbase  16743  lmodplusg  16744  lmodsca  16745  lmodvsca  16746  ipsbase  16750  ipsaddg  16751  ipsmulr  16752  ipssca  16753  ipsvsca  16754  ipsip  16755  phlbase  16760  phlplusg  16761  phlsca  16762  phlvsca  16763  phlip  16764  topgrpbas  16768  topgrpplusg  16769  topgrptset  16770  otpsbas  16775  otpstset  16776  otpsle  16777  odrngbas  16786  odrngplusg  16787  odrngmulr  16788  odrngtset  16789  odrngle  16790  odrngds  16791  homarw  17421  ipoval  17883  ipolerval  17885  eqgfval  18449  cycsubg  18472  symgbas  18620  symgsubmefmndALT  18652  islbs3  20049  cnfldbas  20224  cnfldadd  20225  cnfldmul  20226  cnfldcj  20227  cnfldtset  20228  cnfldle  20229  cnfldds  20230  cnfldunif  20231  basdif0  21707  iscldtop  21849  iocpnfordt  21969  icomnfordt  21970  iooordt  21971  cnrest2  22040  cmpcov2  22144  fiuncmp  22158  bwth  22164  indisconn  22172  locfincmp  22280  xkococnlem  22413  hmphdis  22550  uzrest  22651  ufildr  22685  fin1aufil  22686  eltsms  22887  ustval  22957  qtopbaslem  23514  tgqioo  23555  re2ndc  23556  xrhmeo  23701  bndth  23713  pi1xfrcnvlem  23811  ovolficcss  24224  nulmbl2  24291  uniiccdif  24333  opnmbllem  24356  opnmblALT  24358  mbfimaopnlem  24410  i1fima  24433  i1fima2  24434  i1fd  24436  c1liplem1  24751  deg1n0ima  24845  efcvx  25199  dvrelog  25383  dvloglem  25394  logf1o2  25396  dvlog  25397  ressatans  25675  wilthlem3  25810  trkgbas  26394  trkgdist  26395  trkgitv  26396  ex-ss  28367  ajfval  28747  ipasslem8  28775  hlimcaui  29174  shsspwh  29184  hhssabloi  29200  hhssnv  29202  hhshsslem1  29205  shunssji  29307  sshhococi  29484  pjoml6i  29527  osumcori  29581  mayete3i  29666  mayetes3i  29667  imaelshi  29996  pjclem1  30133  pjci  30138  mdcompli  30367  dmdcompli  30368  xppreima  30560  gsummpt2co  30888  cycpmrn  30990  circtopn  31362  esumpcvgval  31619  esumcvg  31627  ldgenpisyslem3  31706  elmbfmvol2  31807  sxbrsigalem0  31811  eulerpartlemsv3  31901  ballotlem7  32075  rpsqrtcn  32146  bnj931  32324  bnj1137  32549  subfacp1lem2a  32716  subfacp1lem2b  32717  erdszelem2  32728  kur14lem7  32748  kur14lem9  32750  dfon2lem2  33337  frrlem12  33457  bday1s  33671  bj-snglsstag  34817  bj-2upln1upl  34860  bj-0int  34916  bj-opabssvv  34965  bj-ccssccbar  35032  bj-ccinftyssccbar  35033  bj-rvecsscvec  35118  icoreelrn  35178  finxpreclem3  35210  imadifss  35398  poimirlem4  35427  poimirlem26  35449  poimirlem27  35450  opnmbllem0  35459  mblfinlem3  35462  mblfinlem4  35463  ismblfin  35464  volsupnfl  35468  sdclem2  35546  heibor1lem  35613  refrelsredund4  36391  dicval  38836  dvhdimlem  39104  ismrc  40118  mapfzcons1cl  40135  2rexfrabdioph  40213  3rexfrabdioph  40214  4rexfrabdioph  40215  6rexfrabdioph  40216  7rexfrabdioph  40217  rabdiophlem2  40219  jm2.27dlem5  40430  algbase  40598  algaddg  40599  algmulr  40600  algsca  40601  algvsca  40602  intimass2  40832  comptiunov2i  40883  relexp0a  40893  lhe4.4ex1a  41508  iocnct  42641  iccnct  42642  dvcosre  43018  fourierdlem46  43258  fourierdlem57  43269  fourierdlem58  43270  fourierdlem62  43274  fourierdlem102  43314  fourierdlem103  43315  fourierdlem104  43316  fourierdlem114  43326  sge0split  43512  sge0uzfsumgt  43547  hoiprodp1  43691  hoidmvlelem1  43698  hoidmvlelem2  43699  hoidmvlelem3  43700  sbgoldbo  44803  dmmpossx2  45236  aacllem  45988