Theorem sseqtrri 3952

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

Syntax hints:   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqimss2i  3974  difsssymdif  4179  snsspr1  4707  snsspr2  4708  snsstp1  4709  snsstp2  4710  snsstp3  4711  unissint  4862  iunxdif2  4940  pwpwssunieq  4989  intabs  5209  inxpssres  5536  opabssxp  5607  dmresi  5888  cnvimass  5916  sofld  6011  cnvcnv  6016  cnvssrndm  6090  sssucid  6236  fvclss  6979  dmmpossx  7746  suppun  7833  wfrlem14  7951  tfrlem11  8007  oawordeulem  8163  mapex  8395  trcl  9154  djuunxp  9334  dfac3  9532  cfsuc  9668  isfin4p1  9726  fin23lem11  9728  domtriomlem  9853  ttukeylem1  9920  ttukeylem7  9926  brdom7disj  9942  brdom6disj  9943  fingch  10034  fpwwe2lem13  10053  canthp1lem2  10064  wunex2  10149  wunex3  10152  ressxr  10674  ltrelxr  10691  nnssnn0  11888  un0addcl  11918  un0mulcl  11919  nn0ssxnn0  11958  caubnd  14710  isumclim3  15106  iprodclim3  15346  bpoly4  15405  fprodefsum  15440  znnen  15557  isprm3  16017  phimullem  16106  isstruct2  16485  2strbas  16595  2strop  16596  2strbas1  16598  rngbase  16612  rngplusg  16613  rngmulr  16614  srngbase  16620  srngplusg  16621  srngmulr  16622  srnginvl  16623  lmodbase  16629  lmodplusg  16630  lmodsca  16631  lmodvsca  16632  ipsbase  16636  ipsaddg  16637  ipsmulr  16638  ipssca  16639  ipsvsca  16640  ipsip  16641  phlbase  16646  phlplusg  16647  phlsca  16648  phlvsca  16649  phlip  16650  topgrpbas  16654  topgrpplusg  16655  topgrptset  16656  otpsbas  16661  otpstset  16662  otpsle  16663  odrngbas  16672  odrngplusg  16673  odrngmulr  16674  odrngtset  16675  odrngle  16676  odrngds  16677  homarw  17298  ipoval  17756  ipolerval  17758  eqgfval  18320  cycsubg  18343  symgbas  18491  symgsubmefmndALT  18523  islbs3  19920  cnfldbas  20095  cnfldadd  20096  cnfldmul  20097  cnfldcj  20098  cnfldtset  20099  cnfldle  20100  cnfldds  20101  cnfldunif  20102  basdif0  21558  iscldtop  21700  iocpnfordt  21820  icomnfordt  21821  iooordt  21822  cnrest2  21891  cmpcov2  21995  fiuncmp  22009  bwth  22015  indisconn  22023  locfincmp  22131  xkococnlem  22264  hmphdis  22401  uzrest  22502  ufildr  22536  fin1aufil  22537  eltsms  22738  ustval  22808  qtopbaslem  23364  tgqioo  23405  re2ndc  23406  xrhmeo  23551  bndth  23563  pi1xfrcnvlem  23661  ovolficcss  24073  nulmbl2  24140  uniiccdif  24182  opnmbllem  24205  opnmblALT  24207  mbfimaopnlem  24259  i1fima  24282  i1fima2  24283  i1fd  24285  c1liplem1  24599  deg1n0ima  24690  efcvx  25044  dvrelog  25228  dvloglem  25239  logf1o2  25241  dvlog  25242  ressatans  25520  wilthlem3  25655  trkgbas  26239  trkgdist  26240  trkgitv  26241  ex-ss  28212  ajfval  28592  ipasslem8  28620  hlimcaui  29019  shsspwh  29029  hhssabloi  29045  hhssnv  29047  hhshsslem1  29050  shunssji  29152  sshhococi  29329  pjoml6i  29372  osumcori  29426  mayete3i  29511  mayetes3i  29512  imaelshi  29841  pjclem1  29978  pjci  29983  mdcompli  30212  dmdcompli  30213  xppreima  30408  gsummpt2co  30733  cycpmrn  30835  circtopn  31190  esumpcvgval  31447  esumcvg  31455  ldgenpisyslem3  31534  elmbfmvol2  31635  sxbrsigalem0  31639  eulerpartlemsv3  31729  ballotlem7  31903  rpsqrtcn  31974  bnj931  32152  bnj1137  32377  subfacp1lem2a  32540  subfacp1lem2b  32541  erdszelem2  32552  kur14lem7  32572  kur14lem9  32574  dfon2lem2  33142  frrlem12  33247  bj-snglsstag  34417  bj-2upln1upl  34460  bj-0int  34516  bj-opabssvv  34565  bj-ccssccbar  34632  bj-ccinftyssccbar  34633  bj-rvecsscvec  34718  icoreelrn  34778  finxpreclem3  34810  imadifss  35032  poimirlem4  35061  poimirlem26  35083  poimirlem27  35084  opnmbllem0  35093  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  volsupnfl  35102  sdclem2  35180  heibor1lem  35247  refrelsredund4  36027  dicval  38472  dvhdimlem  38740  ismrc  39642  mapfzcons1cl  39659  2rexfrabdioph  39737  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  rabdiophlem2  39743  jm2.27dlem5  39954  algbase  40122  algaddg  40123  algmulr  40124  algsca  40125  algvsca  40126  intimass2  40356  comptiunov2i  40407  relexp0a  40417  lhe4.4ex1a  41033  iocnct  42177  iccnct  42178  dvcosre  42554  fourierdlem46  42794  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  sge0split  43048  sge0uzfsumgt  43083  hoiprodp1  43227  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  sbgoldbo  44305  dmmpossx2  44738  aacllem  45329