Theorem sseqtrri 4004

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

Syntax hints:   = wceq 1537   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqimss2i  4026  difsssymdif  4229  snsspr1  4747  snsspr2  4748  snsstp1  4749  snsstp2  4750  snsstp3  4751  unissint  4900  iunxdif2  4977  pwpwssunieq  5026  intabs  5245  inxpssres  5572  opabssxp  5643  dmresi  5921  cnvimass  5949  sofld  6044  cnvcnv  6049  cnvssrndm  6122  sssucid  6268  fvclss  7001  dmmpossx  7764  suppun  7850  wfrlem14  7968  tfrlem11  8024  oawordeulem  8180  mapex  8412  trcl  9170  djuunxp  9350  dfac3  9547  cfsuc  9679  isfin4p1  9737  fin23lem11  9739  domtriomlem  9864  ttukeylem1  9931  ttukeylem7  9937  brdom7disj  9953  brdom6disj  9954  fingch  10045  fpwwe2lem13  10064  canthp1lem2  10075  wunex2  10160  wunex3  10163  ressxr  10685  ltrelxr  10702  nnssnn0  11901  un0addcl  11931  un0mulcl  11932  nn0ssxnn0  11971  caubnd  14718  isumclim3  15114  iprodclim3  15354  bpoly4  15413  fprodefsum  15448  znnen  15565  isprm3  16027  phimullem  16116  isstruct2  16493  2strbas  16603  2strop  16604  2strbas1  16606  rngbase  16620  rngplusg  16621  rngmulr  16622  srngbase  16628  srngplusg  16629  srngmulr  16630  srnginvl  16631  lmodbase  16637  lmodplusg  16638  lmodsca  16639  lmodvsca  16640  ipsbase  16644  ipsaddg  16645  ipsmulr  16646  ipssca  16647  ipsvsca  16648  ipsip  16649  phlbase  16654  phlplusg  16655  phlsca  16656  phlvsca  16657  phlip  16658  topgrpbas  16662  topgrpplusg  16663  topgrptset  16664  otpsbas  16669  otpstset  16670  otpsle  16671  odrngbas  16680  odrngplusg  16681  odrngmulr  16682  odrngtset  16683  odrngle  16684  odrngds  16685  homarw  17306  ipoval  17764  ipolerval  17766  eqgfval  18328  cycsubg  18351  symgbas  18499  symgsubmefmndALT  18531  islbs3  19927  cnfldbas  20549  cnfldadd  20550  cnfldmul  20551  cnfldcj  20552  cnfldtset  20553  cnfldle  20554  cnfldds  20555  cnfldunif  20556  basdif0  21561  iscldtop  21703  iocpnfordt  21823  icomnfordt  21824  iooordt  21825  cnrest2  21894  cmpcov2  21998  fiuncmp  22012  bwth  22018  indisconn  22026  locfincmp  22134  xkococnlem  22267  hmphdis  22404  uzrest  22505  ufildr  22539  fin1aufil  22540  eltsms  22741  ustval  22811  qtopbaslem  23367  tgqioo  23408  re2ndc  23409  xrhmeo  23550  bndth  23562  pi1xfrcnvlem  23660  ovolficcss  24070  nulmbl2  24137  uniiccdif  24179  opnmbllem  24202  opnmblALT  24204  mbfimaopnlem  24256  i1fima  24279  i1fima2  24280  i1fd  24282  c1liplem1  24593  deg1n0ima  24683  efcvx  25037  dvrelog  25220  dvloglem  25231  logf1o2  25233  dvlog  25234  ressatans  25512  wilthlem3  25647  trkgbas  26231  trkgdist  26232  trkgitv  26233  ex-ss  28206  ajfval  28586  ipasslem8  28614  hlimcaui  29013  shsspwh  29023  hhssabloi  29039  hhssnv  29041  hhshsslem1  29044  shunssji  29146  sshhococi  29323  pjoml6i  29366  osumcori  29420  mayete3i  29505  mayetes3i  29506  imaelshi  29835  pjclem1  29972  pjci  29977  mdcompli  30206  dmdcompli  30207  xppreima  30394  gsummpt2co  30686  cycpmrn  30785  circtopn  31101  esumpcvgval  31337  esumcvg  31345  ldgenpisyslem3  31424  elmbfmvol2  31525  sxbrsigalem0  31529  eulerpartlemsv3  31619  ballotlem7  31793  rpsqrtcn  31864  bnj931  32042  bnj1137  32267  subfacp1lem2a  32427  subfacp1lem2b  32428  erdszelem2  32439  kur14lem7  32459  kur14lem9  32461  dfon2lem2  33029  frrlem12  33134  bj-snglsstag  34296  bj-2upln1upl  34339  bj-0int  34396  bj-opabssvv  34445  bj-ccssccbar  34502  bj-ccinftyssccbar  34503  bj-rvecsscvec  34588  icoreelrn  34645  finxpreclem3  34677  imadifss  34882  poimirlem4  34911  poimirlem26  34933  poimirlem27  34934  opnmbllem0  34943  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  volsupnfl  34952  sdclem2  35032  heibor1lem  35102  refrelsredund4  35882  dicval  38327  dvhdimlem  38595  ismrc  39347  mapfzcons1cl  39364  2rexfrabdioph  39442  3rexfrabdioph  39443  4rexfrabdioph  39444  6rexfrabdioph  39445  7rexfrabdioph  39446  rabdiophlem2  39448  jm2.27dlem5  39659  algbase  39827  algaddg  39828  algmulr  39829  algsca  39830  algvsca  39831  intimass2  40049  comptiunov2i  40100  relexp0a  40110  lhe4.4ex1a  40710  iocnct  41865  iccnct  41866  dvcosre  42245  fourierdlem46  42486  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  sge0split  42740  sge0uzfsumgt  42775  hoiprodp1  42919  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  sbgoldbo  44001  dmmpossx2  44434  aacllem  44951