Theorem sseqtrri 3957

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  3sstr4i  3959  eqimss2i  3969  difsssymdif  4208  snsspr1  4769  snsspr2  4770  snsstp1  4771  snsstp2  4772  snsstp3  4773  unissint  4931  iunxdif2  5011  pwpwssunieq  5063  intabs  5309  inxpssres  5667  elopaelxp  5740  opabssxp  5742  dmresi  6043  sofld  6178  cnvcnv  6183  imassrn  6197  cnvimass  6198  imadifssranOLD  6202  cnvssrndm  6273  sssucid  6445  cnvimainrn  7066  fvclss  7245  dmmpossx  8077  suppun  8204  frrlem12  8318  tfrlem11  8399  oawordeulem  8565  trcl  9732  djuunxp  10005  dfac3  10203  cfsuc  10338  isfin4p1  10396  fin23lem11  10398  domtriomlem  10523  ttukeylem1  10590  ttukeylem7  10596  brdom7disj  10613  brdom6disj  10614  fingch  10711  fpwwe2lem12  10730  canthp1lem2  10741  wunex2  10826  wunex3  10829  ressxr  11356  ltrelxr  11373  nnssnn0  12612  un0addcl  12642  un0mulcl  12643  nn0ssxnn0  12685  caubnd  15531  isumclim3  15930  iprodclim3  16172  bpoly4  16230  fprodefsum  16266  znnen  16385  isprm3  16863  phimullem  16961  isstruct2  17332  2strbas  17411  rngbase  17475  rngplusg  17476  rngmulr  17477  srngbase  17486  srngplusg  17487  srngmulr  17488  srnginvl  17489  lmodbase  17502  lmodplusg  17503  lmodsca  17504  lmodvsca  17505  ipsbase  17513  ipsaddg  17514  ipsmulr  17515  ipssca  17516  ipsvsca  17517  ipsip  17518  phlbase  17523  phlplusg  17524  phlsca  17525  phlvsca  17526  phlip  17527  topgrpbas  17538  topgrpplusg  17539  topgrptset  17540  otpsbas  17553  otpstset  17554  otpsle  17555  odrngbas  17580  odrngplusg  17581  odrngmulr  17582  odrngtset  17583  odrngle  17584  odrngds  17585  homarw  18226  ipoval  18709  ipolerval  18711  eqgfval  19393  cycsubg  19428  symgbas  19591  symgsubmefmndALT  19622  islbs3  21438  cnfldbas  21687  mpocnfldadd  21688  mpocnfldmul  21690  cnfldcj  21692  cnfldtset  21693  cnfldle  21694  cnfldds  21695  cnfldunif  21696  basdif0  23276  iscldtop  23418  iocpnfordt  23538  icomnfordt  23539  iooordt  23540  cnrest2  23609  cmpcov2  23713  fiuncmp  23727  bwth  23733  indisconn  23741  locfincmp  23850  xkococnlem  23983  hmphdis  24120  uzrest  24221  ufildr  24255  fin1aufil  24256  eltsms  24457  ustval  24527  qtopbaslem  25082  tgqioo  25124  re2ndc  25125  xrhmeo  25272  bndth  25284  pi1xfrcnvlem  25382  ovolficcss  25795  nulmbl2  25862  uniiccdif  25904  opnmbllem  25927  opnmblALT  25929  mbfimaopnlem  25981  i1fima  26004  i1fima2  26005  i1fd  26007  c1liplem1  26321  deg1n0ima  26412  efcvx  26781  dvrelog  26970  dvloglem  26981  logf1o2  26983  dvlog  26984  ressatans  27267  wilthlem3  27402  bday1  28205  negsproplem2  28420  negbdaylem  28447  oncutlt  28655  oniso  28662  bdayons  28667  bdayn0p1  28760  trkgbas  28912  trkgdist  28913  trkgitv  28914  ex-ss  31033  ajfval  31416  ipasslem8  31444  hlimcaui  31843  shsspwh  31853  hhssabloi  31869  hhssnv  31871  hhshsslem1  31874  shunssji  31976  sshhococi  32153  pjoml6i  32196  osumcori  32250  mayete3i  32335  mayetes3i  32336  imaelshi  32665  pjclem1  32802  pjci  32807  mdcompli  33036  dmdcompli  33037  xppreima  33286  gsummpt2co  33655  cycpmrn  33750  elrgspnsubrunlem2  33855  evl1deg1  34154  evl1deg2  34155  evl1deg3  34156  circtopn  34515  esumpcvgval  34756  esumcvg  34764  ldgenpisyslem3  34844  elmbfmvol2  34945  sxbrsigalem0  34949  eulerpartlemsv3  35039  ballotlem7  35214  rpsqrtcn  35268  bnj931  35447  bnj1137  35671  fineqvnttrclse  35848  subfacp1lem2a  36031  subfacp1lem2b  36032  erdszelem2  36043  kur14lem7  36063  kur14lem9  36065  dfon2lem2  36638  regsfromunir1  37420  bj-snglsstag  37986  bj-2upln1upl  38029  bj-0int  38114  bj-opabssvv  38164  bj-ccssccbar  38231  bj-ccinftyssccbar  38232  bj-rvecsscvec  38318  icoreelrn  38377  finxpreclem3  38409  imadifss  38616  poimirlem4  38635  poimirlem26  38657  poimirlem27  38658  opnmbllem0  38667  mblfinlem3  38670  mblfinlem4  38671  ismblfin  38672  volsupnfl  38676  sdclem2  38769  heibor1lem  38836  refrelsredund4  39741  dicval  42326  dvhdimlem  42594  ismrc  43805  mapfzcons1cl  43822  2rexfrabdioph  43896  3rexfrabdioph  43897  4rexfrabdioph  43898  6rexfrabdioph  43899  7rexfrabdioph  43900  rabdiophlem2  43902  jm2.27dlem5  44113  algbase  44269  algaddg  44270  algmulr  44271  algsca  44272  algvsca  44273  intimass2  44748  comptiunov2i  44799  relexp0a  44809  lhe4.4ex1a  45406  iocnct  46645  iccnct  46646  dvcosre  47015  fourierdlem46  47255  fourierdlem57  47266  fourierdlem58  47267  fourierdlem62  47271  fourierdlem102  47311  fourierdlem103  47312  fourierdlem104  47313  fourierdlem114  47323  sge0split  47512  sge0uzfsumgt  47547  hoiprodp1  47691  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  sbgoldbo  48978  usgrexmpl1lem  49212  usgrexmpl2lem  49217  dmmpossx2  49542  ipoglb0  50201  mreclat  50204  catbas  50441  cathomfval  50442  catcofval  50443  parhomssun  50840  aacllem  51107