Theorem sseqtrri 4008

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

Syntax hints:   = wceq 1540   ⊆ wss 3926

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  3sstr4i  4010  eqimss2i  4020  difsssymdif  4238  snsspr1  4790  snsspr2  4791  snsstp1  4792  snsstp2  4793  snsstp3  4794  unissint  4948  iunxdif2  5029  pwpwssunieq  5080  intabs  5319  inxpssres  5671  elopaelxp  5744  opabssxp  5747  dmresi  6039  cnvimass  6069  sofld  6176  cnvcnv  6181  cnvssrndm  6260  sssucid  6433  f1imadifssran  6621  cnvimainrn  7056  fvclss  7232  dmmpossx  8063  suppun  8181  frrlem12  8294  wfrlem14OLD  8334  tfrlem11  8400  oawordeulem  8564  mapexOLD  8844  trcl  9740  djuunxp  9933  dfac3  10133  cfsuc  10269  isfin4p1  10327  fin23lem11  10329  domtriomlem  10454  ttukeylem1  10521  ttukeylem7  10527  brdom7disj  10543  brdom6disj  10544  fingch  10635  fpwwe2lem12  10654  canthp1lem2  10665  wunex2  10750  wunex3  10753  ressxr  11277  ltrelxr  11294  nnssnn0  12502  un0addcl  12532  un0mulcl  12533  nn0ssxnn0  12575  caubnd  15375  isumclim3  15773  iprodclim3  16014  bpoly4  16073  fprodefsum  16109  znnen  16228  isprm3  16700  phimullem  16796  isstruct2  17166  2strbas  17247  rngbase  17311  rngplusg  17312  rngmulr  17313  srngbase  17322  srngplusg  17323  srngmulr  17324  srnginvl  17325  lmodbase  17338  lmodplusg  17339  lmodsca  17340  lmodvsca  17341  ipsbase  17349  ipsaddg  17350  ipsmulr  17351  ipssca  17352  ipsvsca  17353  ipsip  17354  phlbase  17359  phlplusg  17360  phlsca  17361  phlvsca  17362  phlip  17363  topgrpbas  17374  topgrpplusg  17375  topgrptset  17376  otpsbas  17389  otpstset  17390  otpsle  17391  odrngbas  17416  odrngplusg  17417  odrngmulr  17418  odrngtset  17419  odrngle  17420  odrngds  17421  homarw  18057  ipoval  18538  ipolerval  18540  eqgfval  19157  cycsubg  19189  symgbas  19351  symgsubmefmndALT  19382  islbs3  21114  cnfldbas  21317  mpocnfldadd  21318  mpocnfldmul  21320  cnfldcj  21322  cnfldtset  21323  cnfldle  21324  cnfldds  21325  cnfldunif  21326  cnfldbasOLD  21332  cnfldaddOLD  21333  cnfldmulOLD  21334  cnfldcjOLD  21335  cnfldtsetOLD  21336  cnfldleOLD  21337  cnflddsOLD  21338  cnfldunifOLD  21339  basdif0  22889  iscldtop  23031  iocpnfordt  23151  icomnfordt  23152  iooordt  23153  cnrest2  23222  cmpcov2  23326  fiuncmp  23340  bwth  23346  indisconn  23354  locfincmp  23462  xkococnlem  23595  hmphdis  23732  uzrest  23833  ufildr  23867  fin1aufil  23868  eltsms  24069  ustval  24139  qtopbaslem  24695  tgqioo  24737  re2ndc  24738  xrhmeo  24893  bndth  24906  pi1xfrcnvlem  25005  ovolficcss  25420  nulmbl2  25487  uniiccdif  25529  opnmbllem  25552  opnmblALT  25554  mbfimaopnlem  25606  i1fima  25629  i1fima2  25630  i1fd  25632  c1liplem1  25951  deg1n0ima  26044  efcvx  26409  dvrelog  26596  dvloglem  26607  logf1o2  26609  dvlog  26610  ressatans  26894  wilthlem3  27030  bday1s  27793  negsproplem2  27978  negsbdaylem  28005  trkgbas  28370  trkgdist  28371  trkgitv  28372  ex-ss  30354  ajfval  30736  ipasslem8  30764  hlimcaui  31163  shsspwh  31173  hhssabloi  31189  hhssnv  31191  hhshsslem1  31194  shunssji  31296  sshhococi  31473  pjoml6i  31516  osumcori  31570  mayete3i  31655  mayetes3i  31656  imaelshi  31985  pjclem1  32122  pjci  32127  mdcompli  32356  dmdcompli  32357  xppreima  32569  gsummpt2co  32988  cycpmrn  33100  elrgspnsubrunlem2  33189  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  circtopn  33814  esumpcvgval  34055  esumcvg  34063  ldgenpisyslem3  34142  elmbfmvol2  34245  sxbrsigalem0  34249  eulerpartlemsv3  34339  ballotlem7  34514  rpsqrtcn  34571  bnj931  34747  bnj1137  34972  subfacp1lem2a  35148  subfacp1lem2b  35149  erdszelem2  35160  kur14lem7  35180  kur14lem9  35182  dfon2lem2  35748  bj-snglsstag  36945  bj-2upln1upl  36988  bj-0int  37065  bj-opabssvv  37114  bj-ccssccbar  37181  bj-ccinftyssccbar  37182  bj-rvecsscvec  37268  icoreelrn  37325  finxpreclem3  37357  imadifss  37565  poimirlem4  37594  poimirlem26  37616  poimirlem27  37617  opnmbllem0  37626  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  volsupnfl  37635  sdclem2  37712  heibor1lem  37779  refrelsredund4  38596  dicval  41141  dvhdimlem  41409  ismrc  42671  mapfzcons1cl  42688  2rexfrabdioph  42766  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  rabdiophlem2  42772  jm2.27dlem5  42984  algbase  43145  algaddg  43146  algmulr  43147  algsca  43148  algvsca  43149  intimass2  43626  comptiunov2i  43677  relexp0a  43687  lhe4.4ex1a  44301  iocnct  45517  iccnct  45518  dvcosre  45889  fourierdlem46  46129  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem114  46197  sge0split  46386  sge0uzfsumgt  46421  hoiprodp1  46565  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  sbgoldbo  47749  usgrexmpl1lem  47973  usgrexmpl2lem  47978  dmmpossx2  48260  ipoglb0  48916  mreclat  48919  catbas  49094  cathomfval  49095  catcofval  49096  aacllem  49613