Theorem sseqtrri 4019

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

Syntax hints:   = wceq 1540   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  eqimss2i  4043  difsssymdif  4252  snsspr1  4817  snsspr2  4818  snsstp1  4819  snsstp2  4820  snsstp3  4821  unissint  4976  iunxdif2  5056  pwpwssunieq  5107  intabs  5342  inxpssres  5693  elopaelxp  5765  opabssxp  5768  dmresi  6051  cnvimass  6080  sofld  6186  cnvcnv  6191  cnvssrndm  6270  sssucid  6444  cnvimainrn  7068  fvclss  7243  dmmpossx  8055  suppun  8172  frrlem12  8285  wfrlem14OLD  8325  tfrlem11  8391  oawordeulem  8557  mapex  8829  trcl  9726  djuunxp  9919  dfac3  10119  cfsuc  10255  isfin4p1  10313  fin23lem11  10315  domtriomlem  10440  ttukeylem1  10507  ttukeylem7  10513  brdom7disj  10529  brdom6disj  10530  fingch  10621  fpwwe2lem12  10640  canthp1lem2  10651  wunex2  10736  wunex3  10739  ressxr  11263  ltrelxr  11280  nnssnn0  12480  un0addcl  12510  un0mulcl  12511  nn0ssxnn0  12552  caubnd  15310  isumclim3  15710  iprodclim3  15949  bpoly4  16008  fprodefsum  16043  znnen  16160  isprm3  16625  phimullem  16717  isstruct2  17087  2strbas  17172  2strop  17173  2strbas1  17176  rngbase  17249  rngplusg  17250  rngmulr  17251  srngbase  17260  srngplusg  17261  srngmulr  17262  srnginvl  17263  lmodbase  17276  lmodplusg  17277  lmodsca  17278  lmodvsca  17279  ipsbase  17287  ipsaddg  17288  ipsmulr  17289  ipssca  17290  ipsvsca  17291  ipsip  17292  phlbase  17297  phlplusg  17298  phlsca  17299  phlvsca  17300  phlip  17301  topgrpbas  17312  topgrpplusg  17313  topgrptset  17314  otpsbas  17327  otpstset  17328  otpsle  17329  odrngbas  17354  odrngplusg  17355  odrngmulr  17356  odrngtset  17357  odrngle  17358  odrngds  17359  homarw  18001  ipoval  18488  ipolerval  18490  eqgfval  19093  cycsubg  19124  symgbas  19280  symgsubmefmndALT  19313  islbs3  20914  cnfldbas  21149  cnfldadd  21150  cnfldmul  21151  cnfldcj  21152  cnfldtset  21153  cnfldle  21154  cnfldds  21155  cnfldunif  21156  basdif0  22677  iscldtop  22820  iocpnfordt  22940  icomnfordt  22941  iooordt  22942  cnrest2  23011  cmpcov2  23115  fiuncmp  23129  bwth  23135  indisconn  23143  locfincmp  23251  xkococnlem  23384  hmphdis  23521  uzrest  23622  ufildr  23656  fin1aufil  23657  eltsms  23858  ustval  23928  qtopbaslem  24496  tgqioo  24537  re2ndc  24538  xrhmeo  24692  bndth  24705  pi1xfrcnvlem  24804  ovolficcss  25219  nulmbl2  25286  uniiccdif  25328  opnmbllem  25351  opnmblALT  25353  mbfimaopnlem  25405  i1fima  25428  i1fima2  25429  i1fd  25431  c1liplem1  25749  deg1n0ima  25843  efcvx  26198  dvrelog  26382  dvloglem  26393  logf1o2  26395  dvlog  26396  ressatans  26676  wilthlem3  26811  bday1s  27570  negsproplem2  27743  negsbdaylem  27770  trkgbas  27964  trkgdist  27965  trkgitv  27966  ex-ss  29948  ajfval  30330  ipasslem8  30358  hlimcaui  30757  shsspwh  30767  hhssabloi  30783  hhssnv  30785  hhshsslem1  30788  shunssji  30890  sshhococi  31067  pjoml6i  31110  osumcori  31164  mayete3i  31249  mayetes3i  31250  imaelshi  31579  pjclem1  31716  pjci  31721  mdcompli  31950  dmdcompli  31951  xppreima  32139  gsummpt2co  32471  cycpmrn  32573  circtopn  33116  esumpcvgval  33375  esumcvg  33383  ldgenpisyslem3  33462  elmbfmvol2  33565  sxbrsigalem0  33569  eulerpartlemsv3  33659  ballotlem7  33833  rpsqrtcn  33904  bnj931  34080  bnj1137  34305  subfacp1lem2a  34470  subfacp1lem2b  34471  erdszelem2  34482  kur14lem7  34502  kur14lem9  34504  dfon2lem2  35061  gg-cnfldbas  35476  mpocnfldadd  35477  mpocnfldmul  35478  gg-cnfldcj  35479  gg-cnfldtset  35480  gg-cnfldle  35481  gg-cnfldds  35482  gg-cnfldunif  35483  bj-snglsstag  36166  bj-2upln1upl  36209  bj-0int  36286  bj-opabssvv  36335  bj-ccssccbar  36402  bj-ccinftyssccbar  36403  bj-rvecsscvec  36489  icoreelrn  36546  finxpreclem3  36578  imadifss  36767  poimirlem4  36796  poimirlem26  36818  poimirlem27  36819  opnmbllem0  36828  mblfinlem3  36831  mblfinlem4  36832  ismblfin  36833  volsupnfl  36837  sdclem2  36914  heibor1lem  36981  refrelsredund4  37806  dicval  40351  dvhdimlem  40619  ismrc  41742  mapfzcons1cl  41759  2rexfrabdioph  41837  3rexfrabdioph  41838  4rexfrabdioph  41839  6rexfrabdioph  41840  7rexfrabdioph  41841  rabdiophlem2  41843  jm2.27dlem5  42055  algbase  42223  algaddg  42224  algmulr  42225  algsca  42226  algvsca  42227  intimass2  42709  comptiunov2i  42760  relexp0a  42770  lhe4.4ex1a  43391  iocnct  44552  iccnct  44553  dvcosre  44927  fourierdlem46  45167  fourierdlem57  45178  fourierdlem58  45179  fourierdlem62  45183  fourierdlem102  45223  fourierdlem103  45224  fourierdlem104  45225  fourierdlem114  45235  sge0split  45424  sge0uzfsumgt  45459  hoiprodp1  45603  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  sbgoldbo  46754  dmmpossx2  47101  ipoglb0  47707  mreclat  47710  aacllem  47936