Theorem sseqtrri 3996

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3sstr4i  3998  eqimss2i  4008  difsssymdif  4226  snsspr1  4778  snsspr2  4779  snsstp1  4780  snsstp2  4781  snsstp3  4782  unissint  4936  iunxdif2  5017  pwpwssunieq  5068  intabs  5304  inxpssres  5655  elopaelxp  5728  opabssxp  5731  dmresi  6023  cnvimass  6053  sofld  6160  cnvcnv  6165  cnvssrndm  6244  sssucid  6414  f1imadifssran  6602  cnvimainrn  7039  fvclss  7215  dmmpossx  8045  suppun  8163  frrlem12  8276  tfrlem11  8356  oawordeulem  8518  mapexOLD  8805  trcl  9681  djuunxp  9874  dfac3  10074  cfsuc  10210  isfin4p1  10268  fin23lem11  10270  domtriomlem  10395  ttukeylem1  10462  ttukeylem7  10468  brdom7disj  10484  brdom6disj  10485  fingch  10576  fpwwe2lem12  10595  canthp1lem2  10606  wunex2  10691  wunex3  10694  ressxr  11218  ltrelxr  11235  nnssnn0  12445  un0addcl  12475  un0mulcl  12476  nn0ssxnn0  12518  caubnd  15325  isumclim3  15725  iprodclim3  15966  bpoly4  16025  fprodefsum  16061  znnen  16180  isprm3  16653  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  18008  ipoval  18489  ipolerval  18491  eqgfval  19108  cycsubg  19140  symgbas  19302  symgsubmefmndALT  19333  islbs3  21065  cnfldbas  21268  mpocnfldadd  21269  mpocnfldmul  21271  cnfldcj  21273  cnfldtset  21274  cnfldle  21275  cnfldds  21276  cnfldunif  21277  cnfldbasOLD  21283  cnfldaddOLD  21284  cnfldmulOLD  21285  cnfldcjOLD  21286  cnfldtsetOLD  21287  cnfldleOLD  21288  cnflddsOLD  21289  cnfldunifOLD  21290  basdif0  22840  iscldtop  22982  iocpnfordt  23102  icomnfordt  23103  iooordt  23104  cnrest2  23173  cmpcov2  23277  fiuncmp  23291  bwth  23297  indisconn  23305  locfincmp  23413  xkococnlem  23546  hmphdis  23683  uzrest  23784  ufildr  23818  fin1aufil  23819  eltsms  24020  ustval  24090  qtopbaslem  24646  tgqioo  24688  re2ndc  24689  xrhmeo  24844  bndth  24857  pi1xfrcnvlem  24956  ovolficcss  25370  nulmbl2  25437  uniiccdif  25479  opnmbllem  25502  opnmblALT  25504  mbfimaopnlem  25556  i1fima  25579  i1fima2  25580  i1fd  25582  c1liplem1  25901  deg1n0ima  25994  efcvx  26359  dvrelog  26546  dvloglem  26557  logf1o2  26559  dvlog  26560  ressatans  26844  wilthlem3  26980  bday1s  27743  negsproplem2  27935  negsbdaylem  27962  onscutlt  28165  onsiso  28169  bdayon  28173  bdayn0p1  28258  trkgbas  28372  trkgdist  28373  trkgitv  28374  ex-ss  30356  ajfval  30738  ipasslem8  30766  hlimcaui  31165  shsspwh  31175  hhssabloi  31191  hhssnv  31193  hhshsslem1  31196  shunssji  31298  sshhococi  31475  pjoml6i  31518  osumcori  31572  mayete3i  31657  mayetes3i  31658  imaelshi  31987  pjclem1  32124  pjci  32129  mdcompli  32358  dmdcompli  32359  xppreima  32569  gsummpt2co  32988  cycpmrn  33100  elrgspnsubrunlem2  33199  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  circtopn  33827  esumpcvgval  34068  esumcvg  34076  ldgenpisyslem3  34155  elmbfmvol2  34258  sxbrsigalem0  34262  eulerpartlemsv3  34352  ballotlem7  34527  rpsqrtcn  34584  bnj931  34760  bnj1137  34985  subfacp1lem2a  35167  subfacp1lem2b  35168  erdszelem2  35179  kur14lem7  35199  kur14lem9  35201  dfon2lem2  35772  bj-snglsstag  36969  bj-2upln1upl  37012  bj-0int  37089  bj-opabssvv  37138  bj-ccssccbar  37205  bj-ccinftyssccbar  37206  bj-rvecsscvec  37292  icoreelrn  37349  finxpreclem3  37381  imadifss  37589  poimirlem4  37618  poimirlem26  37640  poimirlem27  37641  opnmbllem0  37650  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  volsupnfl  37659  sdclem2  37736  heibor1lem  37803  refrelsredund4  38623  dicval  41170  dvhdimlem  41438  ismrc  42689  mapfzcons1cl  42706  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  rabdiophlem2  42790  jm2.27dlem5  43002  algbase  43163  algaddg  43164  algmulr  43165  algsca  43166  algvsca  43167  intimass2  43644  comptiunov2i  43695  relexp0a  43705  lhe4.4ex1a  44318  iocnct  45538  iccnct  45539  dvcosre  45910  fourierdlem46  46150  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sge0split  46407  sge0uzfsumgt  46442  hoiprodp1  46586  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  sbgoldbo  47788  usgrexmpl1lem  48012  usgrexmpl2lem  48017  dmmpossx2  48325  ipoglb0  48982  mreclat  48985  catbas  49215  cathomfval  49216  catcofval  49217  aacllem  49790