Theorem sseqtrri 3987

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

Syntax hints:   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  3sstr4i  3989  eqimss2i  3999  difsssymdif  4217  snsspr1  4781  snsspr2  4782  snsstp1  4783  snsstp2  4784  snsstp3  4785  unissint  4938  iunxdif2  5019  pwpwssunieq  5071  intabs  5321  inxpssres  5680  elopaelxp  5753  opabssxp  5755  dmresi  6056  cnvimass  6086  sofld  6187  cnvcnv  6192  imadifssran  6204  cnvssrndm  6274  sssucid  6445  cnvimainrn  7064  fvclss  7241  dmmpossx  8064  suppun  8181  frrlem12  8295  tfrlem11  8376  oawordeulem  8540  trcl  9698  djuunxp  9908  dfac3  10106  cfsuc  10242  isfin4p1  10300  fin23lem11  10302  domtriomlem  10427  ttukeylem1  10494  ttukeylem7  10500  brdom7disj  10516  brdom6disj  10517  fingch  10609  fpwwe2lem12  10628  canthp1lem2  10639  wunex2  10724  wunex3  10727  ressxr  11254  ltrelxr  11271  nnssnn0  12508  un0addcl  12538  un0mulcl  12539  nn0ssxnn0  12581  caubnd  15412  isumclim3  15812  iprodclim3  16056  bpoly4  16114  fprodefsum  16150  znnen  16269  isprm3  16742  phimullem  16839  isstruct2  17210  2strbas  17289  rngbase  17353  rngplusg  17354  rngmulr  17355  srngbase  17364  srngplusg  17365  srngmulr  17366  srnginvl  17367  lmodbase  17380  lmodplusg  17381  lmodsca  17382  lmodvsca  17383  ipsbase  17391  ipsaddg  17392  ipsmulr  17393  ipssca  17394  ipsvsca  17395  ipsip  17396  phlbase  17401  phlplusg  17402  phlsca  17403  phlvsca  17404  phlip  17405  topgrpbas  17416  topgrpplusg  17417  topgrptset  17418  otpsbas  17431  otpstset  17432  otpsle  17433  odrngbas  17458  odrngplusg  17459  odrngmulr  17460  odrngtset  17461  odrngle  17462  odrngds  17463  homarw  18104  ipoval  18587  ipolerval  18589  eqgfval  19245  cycsubg  19280  symgbas  19443  symgsubmefmndALT  19474  islbs3  21260  cnfldbas  21507  mpocnfldadd  21508  mpocnfldmul  21510  cnfldcj  21512  cnfldtset  21513  cnfldle  21514  cnfldds  21515  cnfldunif  21516  basdif0  23091  iscldtop  23233  iocpnfordt  23353  icomnfordt  23354  iooordt  23355  cnrest2  23424  cmpcov2  23528  fiuncmp  23542  bwth  23548  indisconn  23556  locfincmp  23664  xkococnlem  23797  hmphdis  23934  uzrest  24035  ufildr  24069  fin1aufil  24070  eltsms  24271  ustval  24341  qtopbaslem  24896  tgqioo  24938  re2ndc  24939  xrhmeo  25086  bndth  25098  pi1xfrcnvlem  25196  ovolficcss  25609  nulmbl2  25676  uniiccdif  25718  opnmbllem  25741  opnmblALT  25743  mbfimaopnlem  25795  i1fima  25818  i1fima2  25819  i1fd  25821  c1liplem1  26136  deg1n0ima  26227  efcvx  26590  dvrelog  26780  dvloglem  26791  logf1o2  26793  dvlog  26794  ressatans  27077  wilthlem3  27212  bday1  27985  negsproplem2  28200  negbdaylem  28227  oncutlt  28435  oniso  28442  bdayons  28447  bdayn0p1  28540  trkgbas  28692  trkgdist  28693  trkgitv  28694  ex-ss  30756  ajfval  31139  ipasslem8  31167  hlimcaui  31566  shsspwh  31576  hhssabloi  31592  hhssnv  31594  hhshsslem1  31597  shunssji  31699  sshhococi  31876  pjoml6i  31919  osumcori  31973  mayete3i  32058  mayetes3i  32059  imaelshi  32388  pjclem1  32525  pjci  32530  mdcompli  32759  dmdcompli  32760  xppreima  32968  gsummpt2co  33346  cycpmrn  33441  elrgspnsubrunlem2  33546  evl1deg1  33844  evl1deg2  33845  evl1deg3  33846  circtopn  34205  esumpcvgval  34446  esumcvg  34454  ldgenpisyslem3  34533  elmbfmvol2  34635  sxbrsigalem0  34639  eulerpartlemsv3  34729  ballotlem7  34904  rpsqrtcn  34958  bnj931  35137  bnj1137  35361  fineqvnttrclse  35515  subfacp1lem2a  35650  subfacp1lem2b  35651  erdszelem2  35662  kur14lem7  35682  kur14lem9  35684  dfon2lem2  36252  regsfromunir1  37029  bj-snglsstag  37595  bj-2upln1upl  37638  bj-0int  37721  bj-opabssvv  37772  bj-ccssccbar  37839  bj-ccinftyssccbar  37840  bj-rvecsscvec  37926  icoreelrn  37985  finxpreclem3  38017  imadifss  38224  poimirlem4  38253  poimirlem26  38275  poimirlem27  38276  opnmbllem0  38285  mblfinlem3  38288  mblfinlem4  38289  ismblfin  38290  volsupnfl  38294  sdclem2  38371  heibor1lem  38438  refrelsredund4  39343  dicval  41928  dvhdimlem  42196  ismrc  43412  mapfzcons1cl  43429  2rexfrabdioph  43503  3rexfrabdioph  43504  4rexfrabdioph  43505  6rexfrabdioph  43506  7rexfrabdioph  43507  rabdiophlem2  43509  jm2.27dlem5  43720  algbase  43881  algaddg  43882  algmulr  43883  algsca  43884  algvsca  43885  intimass2  44361  comptiunov2i  44412  relexp0a  44422  lhe4.4ex1a  45019  iocnct  46236  iccnct  46237  dvcosre  46606  fourierdlem46  46846  fourierdlem57  46857  fourierdlem58  46858  fourierdlem62  46862  fourierdlem102  46902  fourierdlem103  46903  fourierdlem104  46904  fourierdlem114  46914  sge0split  47103  sge0uzfsumgt  47138  hoiprodp1  47282  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  sbgoldbo  48529  usgrexmpl1lem  48763  usgrexmpl2lem  48768  dmmpossx2  49094  ipoglb0  49749  mreclat  49752  catbas  49981  cathomfval  49982  catcofval  49983  aacllem  50578