Theorem sseqtrri 3988

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

Syntax hints:   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  3sstr4i  3990  eqimss2i  4000  difsssymdif  4218  snsspr1  4775  snsspr2  4776  snsstp1  4777  snsstp2  4778  snsstp3  4779  unissint  4933  iunxdif2  5014  pwpwssunieq  5066  intabs  5310  inxpssres  5669  elopaelxp  5742  opabssxp  5744  dmresi  6045  cnvimass  6075  sofld  6177  cnvcnv  6182  cnvssrndm  6262  sssucid  6432  f1imadifssran  6611  cnvimainrn  7052  fvclss  7229  dmmpossx  8051  suppun  8168  frrlem12  8282  tfrlem11  8363  oawordeulem  8527  trcl  9685  djuunxp  9895  dfac3  10093  cfsuc  10229  isfin4p1  10287  fin23lem11  10289  domtriomlem  10414  ttukeylem1  10481  ttukeylem7  10487  brdom7disj  10503  brdom6disj  10504  fingch  10596  fpwwe2lem12  10615  canthp1lem2  10626  wunex2  10711  wunex3  10714  ressxr  11241  ltrelxr  11258  nnssnn0  12498  un0addcl  12528  un0mulcl  12529  nn0ssxnn0  12571  caubnd  15400  isumclim3  15800  iprodclim3  16044  bpoly4  16103  fprodefsum  16139  znnen  16258  isprm3  16731  phimullem  16828  isstruct2  17199  2strbas  17278  rngbase  17342  rngplusg  17343  rngmulr  17344  srngbase  17353  srngplusg  17354  srngmulr  17355  srnginvl  17356  lmodbase  17369  lmodplusg  17370  lmodsca  17371  lmodvsca  17372  ipsbase  17380  ipsaddg  17381  ipsmulr  17382  ipssca  17383  ipsvsca  17384  ipsip  17385  phlbase  17390  phlplusg  17391  phlsca  17392  phlvsca  17393  phlip  17394  topgrpbas  17405  topgrpplusg  17406  topgrptset  17407  otpsbas  17420  otpstset  17421  otpsle  17422  odrngbas  17447  odrngplusg  17448  odrngmulr  17449  odrngtset  17450  odrngle  17451  odrngds  17452  homarw  18093  ipoval  18576  ipolerval  18578  eqgfval  19235  cycsubg  19270  symgbas  19433  symgsubmefmndALT  19464  islbs3  21248  cnfldbas  21486  mpocnfldadd  21487  mpocnfldmul  21489  cnfldcj  21491  cnfldtset  21492  cnfldle  21493  cnfldds  21494  cnfldunif  21495  basdif0  23071  iscldtop  23213  iocpnfordt  23333  icomnfordt  23334  iooordt  23335  cnrest2  23404  cmpcov2  23508  fiuncmp  23522  bwth  23528  indisconn  23536  locfincmp  23644  xkococnlem  23777  hmphdis  23914  uzrest  24015  ufildr  24049  fin1aufil  24050  eltsms  24251  ustval  24321  qtopbaslem  24876  tgqioo  24918  re2ndc  24919  xrhmeo  25066  bndth  25078  pi1xfrcnvlem  25176  ovolficcss  25589  nulmbl2  25656  uniiccdif  25698  opnmbllem  25721  opnmblALT  25723  mbfimaopnlem  25775  i1fima  25798  i1fima2  25799  i1fd  25801  c1liplem1  26116  deg1n0ima  26207  efcvx  26570  dvrelog  26760  dvloglem  26771  logf1o2  26773  dvlog  26774  ressatans  27057  wilthlem3  27192  bday1  27965  negsproplem2  28180  negbdaylem  28207  oncutlt  28415  oniso  28422  bdayons  28427  bdayn0p1  28520  trkgbas  28672  trkgdist  28673  trkgitv  28674  ex-ss  30687  ajfval  31070  ipasslem8  31098  hlimcaui  31497  shsspwh  31507  hhssabloi  31523  hhssnv  31525  hhshsslem1  31528  shunssji  31630  sshhococi  31807  pjoml6i  31850  osumcori  31904  mayete3i  31989  mayetes3i  31990  imaelshi  32319  pjclem1  32456  pjci  32461  mdcompli  32690  dmdcompli  32691  xppreima  32902  gsummpt2co  33281  cycpmrn  33376  elrgspnsubrunlem2  33481  evl1deg1  33783  evl1deg2  33784  evl1deg3  33785  circtopn  34144  esumpcvgval  34385  esumcvg  34393  ldgenpisyslem3  34472  elmbfmvol2  34574  sxbrsigalem0  34578  eulerpartlemsv3  34668  ballotlem7  34843  rpsqrtcn  34897  bnj931  35076  bnj1137  35300  fineqvnttrclse  35432  subfacp1lem2a  35543  subfacp1lem2b  35544  erdszelem2  35555  kur14lem7  35575  kur14lem9  35577  dfon2lem2  36145  regsfromunir1  36913  bj-snglsstag  37478  bj-2upln1upl  37521  bj-0int  37603  bj-opabssvv  37654  bj-ccssccbar  37721  bj-ccinftyssccbar  37722  bj-rvecsscvec  37808  icoreelrn  37867  finxpreclem3  37899  imadifss  38106  poimirlem4  38135  poimirlem26  38157  poimirlem27  38158  opnmbllem0  38167  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  volsupnfl  38176  sdclem2  38253  heibor1lem  38320  refrelsredund4  39227  dicval  41812  dvhdimlem  42080  ismrc  43294  mapfzcons1cl  43311  2rexfrabdioph  43385  3rexfrabdioph  43386  4rexfrabdioph  43387  6rexfrabdioph  43388  7rexfrabdioph  43389  rabdiophlem2  43391  jm2.27dlem5  43602  algbase  43763  algaddg  43764  algmulr  43765  algsca  43766  algvsca  43767  intimass2  44243  comptiunov2i  44294  relexp0a  44304  lhe4.4ex1a  44903  iocnct  46114  iccnct  46115  dvcosre  46484  fourierdlem46  46724  fourierdlem57  46735  fourierdlem58  46736  fourierdlem62  46740  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem114  46792  sge0split  46981  sge0uzfsumgt  47016  hoiprodp1  47160  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  sbgoldbo  48407  usgrexmpl1lem  48641  usgrexmpl2lem  48646  dmmpossx2  48968  ipoglb0  49623  mreclat  49626  catbas  49855  cathomfval  49856  catcofval  49857  aacllem  50430