Theorem sseqtrri 4018

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

Syntax hints:   = wceq 1539   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  eqimss2i  4042  difsssymdif  4251  snsspr1  4816  snsspr2  4817  snsstp1  4818  snsstp2  4819  snsstp3  4820  unissint  4975  iunxdif2  5055  pwpwssunieq  5106  intabs  5341  inxpssres  5692  elopaelxp  5764  opabssxp  5767  dmresi  6050  cnvimass  6079  sofld  6185  cnvcnv  6190  cnvssrndm  6269  sssucid  6443  cnvimainrn  7067  fvclss  7242  dmmpossx  8054  suppun  8171  frrlem12  8284  wfrlem14OLD  8324  tfrlem11  8390  oawordeulem  8556  mapex  8828  trcl  9725  djuunxp  9918  dfac3  10118  cfsuc  10254  isfin4p1  10312  fin23lem11  10314  domtriomlem  10439  ttukeylem1  10506  ttukeylem7  10512  brdom7disj  10528  brdom6disj  10529  fingch  10620  fpwwe2lem12  10639  canthp1lem2  10650  wunex2  10735  wunex3  10738  ressxr  11262  ltrelxr  11279  nnssnn0  12479  un0addcl  12509  un0mulcl  12510  nn0ssxnn0  12551  caubnd  15309  isumclim3  15709  iprodclim3  15948  bpoly4  16007  fprodefsum  16042  znnen  16159  isprm3  16624  phimullem  16716  isstruct2  17086  2strbas  17171  2strop  17172  2strbas1  17175  rngbase  17248  rngplusg  17249  rngmulr  17250  srngbase  17259  srngplusg  17260  srngmulr  17261  srnginvl  17262  lmodbase  17275  lmodplusg  17276  lmodsca  17277  lmodvsca  17278  ipsbase  17286  ipsaddg  17287  ipsmulr  17288  ipssca  17289  ipsvsca  17290  ipsip  17291  phlbase  17296  phlplusg  17297  phlsca  17298  phlvsca  17299  phlip  17300  topgrpbas  17311  topgrpplusg  17312  topgrptset  17313  otpsbas  17326  otpstset  17327  otpsle  17328  odrngbas  17353  odrngplusg  17354  odrngmulr  17355  odrngtset  17356  odrngle  17357  odrngds  17358  homarw  18000  ipoval  18487  ipolerval  18489  eqgfval  19092  cycsubg  19123  symgbas  19279  symgsubmefmndALT  19312  islbs3  20913  cnfldbas  21148  cnfldadd  21149  cnfldmul  21150  cnfldcj  21151  cnfldtset  21152  cnfldle  21153  cnfldds  21154  cnfldunif  21155  basdif0  22676  iscldtop  22819  iocpnfordt  22939  icomnfordt  22940  iooordt  22941  cnrest2  23010  cmpcov2  23114  fiuncmp  23128  bwth  23134  indisconn  23142  locfincmp  23250  xkococnlem  23383  hmphdis  23520  uzrest  23621  ufildr  23655  fin1aufil  23656  eltsms  23857  ustval  23927  qtopbaslem  24495  tgqioo  24536  re2ndc  24537  xrhmeo  24691  bndth  24704  pi1xfrcnvlem  24803  ovolficcss  25218  nulmbl2  25285  uniiccdif  25327  opnmbllem  25350  opnmblALT  25352  mbfimaopnlem  25404  i1fima  25427  i1fima2  25428  i1fd  25430  c1liplem1  25748  deg1n0ima  25842  efcvx  26197  dvrelog  26381  dvloglem  26392  logf1o2  26394  dvlog  26395  ressatans  26675  wilthlem3  26810  bday1s  27569  negsproplem2  27742  negsbdaylem  27769  trkgbas  27963  trkgdist  27964  trkgitv  27965  ex-ss  29947  ajfval  30329  ipasslem8  30357  hlimcaui  30756  shsspwh  30766  hhssabloi  30782  hhssnv  30784  hhshsslem1  30787  shunssji  30889  sshhococi  31066  pjoml6i  31109  osumcori  31163  mayete3i  31248  mayetes3i  31249  imaelshi  31578  pjclem1  31715  pjci  31720  mdcompli  31949  dmdcompli  31950  xppreima  32138  gsummpt2co  32470  cycpmrn  32572  circtopn  33115  esumpcvgval  33374  esumcvg  33382  ldgenpisyslem3  33461  elmbfmvol2  33564  sxbrsigalem0  33568  eulerpartlemsv3  33658  ballotlem7  33832  rpsqrtcn  33903  bnj931  34079  bnj1137  34304  subfacp1lem2a  34469  subfacp1lem2b  34470  erdszelem2  34481  kur14lem7  34501  kur14lem9  34503  dfon2lem2  35060  gg-cnfldbas  35475  mpocnfldadd  35476  mpocnfldmul  35477  gg-cnfldcj  35478  gg-cnfldtset  35479  gg-cnfldle  35480  gg-cnfldds  35481  gg-cnfldunif  35482  bj-snglsstag  36165  bj-2upln1upl  36208  bj-0int  36285  bj-opabssvv  36334  bj-ccssccbar  36401  bj-ccinftyssccbar  36402  bj-rvecsscvec  36488  icoreelrn  36545  finxpreclem3  36577  imadifss  36766  poimirlem4  36795  poimirlem26  36817  poimirlem27  36818  opnmbllem0  36827  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  volsupnfl  36836  sdclem2  36913  heibor1lem  36980  refrelsredund4  37805  dicval  40350  dvhdimlem  40618  ismrc  41741  mapfzcons1cl  41758  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  rabdiophlem2  41842  jm2.27dlem5  42054  algbase  42222  algaddg  42223  algmulr  42224  algsca  42225  algvsca  42226  intimass2  42708  comptiunov2i  42759  relexp0a  42769  lhe4.4ex1a  43390  iocnct  44551  iccnct  44552  dvcosre  44926  fourierdlem46  45166  fourierdlem57  45177  fourierdlem58  45178  fourierdlem62  45182  fourierdlem102  45222  fourierdlem103  45223  fourierdlem104  45224  fourierdlem114  45234  sge0split  45423  sge0uzfsumgt  45458  hoiprodp1  45602  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  sbgoldbo  46753  dmmpossx2  47100  ipoglb0  47706  mreclat  47709  aacllem  47935