Theorem sseqtrri 3987

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

Syntax hints:   = wceq 1540   ⊆ wss 3905

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  3sstr4i  3989  eqimss2i  3999  difsssymdif  4216  snsspr1  4768  snsspr2  4769  snsstp1  4770  snsstp2  4771  snsstp3  4772  unissint  4925  iunxdif2  5005  pwpwssunieq  5056  intabs  5291  inxpssres  5640  elopaelxp  5713  opabssxp  5715  dmresi  6007  cnvimass  6037  sofld  6140  cnvcnv  6145  cnvssrndm  6223  sssucid  6393  f1imadifssran  6572  cnvimainrn  7005  fvclss  7181  dmmpossx  8008  suppun  8124  frrlem12  8237  tfrlem11  8317  oawordeulem  8479  mapexOLD  8766  trcl  9643  djuunxp  9836  dfac3  10034  cfsuc  10170  isfin4p1  10228  fin23lem11  10230  domtriomlem  10355  ttukeylem1  10422  ttukeylem7  10428  brdom7disj  10444  brdom6disj  10445  fingch  10536  fpwwe2lem12  10555  canthp1lem2  10566  wunex2  10651  wunex3  10654  ressxr  11178  ltrelxr  11195  nnssnn0  12405  un0addcl  12435  un0mulcl  12436  nn0ssxnn0  12478  caubnd  15284  isumclim3  15684  iprodclim3  15925  bpoly4  15984  fprodefsum  16020  znnen  16139  isprm3  16612  phimullem  16708  isstruct2  17078  2strbas  17157  rngbase  17221  rngplusg  17222  rngmulr  17223  srngbase  17232  srngplusg  17233  srngmulr  17234  srnginvl  17235  lmodbase  17248  lmodplusg  17249  lmodsca  17250  lmodvsca  17251  ipsbase  17259  ipsaddg  17260  ipsmulr  17261  ipssca  17262  ipsvsca  17263  ipsip  17264  phlbase  17269  phlplusg  17270  phlsca  17271  phlvsca  17272  phlip  17273  topgrpbas  17284  topgrpplusg  17285  topgrptset  17286  otpsbas  17299  otpstset  17300  otpsle  17301  odrngbas  17326  odrngplusg  17327  odrngmulr  17328  odrngtset  17329  odrngle  17330  odrngds  17331  homarw  17971  ipoval  18454  ipolerval  18456  eqgfval  19073  cycsubg  19105  symgbas  19269  symgsubmefmndALT  19300  islbs3  21080  cnfldbas  21283  mpocnfldadd  21284  mpocnfldmul  21286  cnfldcj  21288  cnfldtset  21289  cnfldle  21290  cnfldds  21291  cnfldunif  21292  cnfldbasOLD  21298  cnfldaddOLD  21299  cnfldmulOLD  21300  cnfldcjOLD  21301  cnfldtsetOLD  21302  cnfldleOLD  21303  cnflddsOLD  21304  cnfldunifOLD  21305  basdif0  22856  iscldtop  22998  iocpnfordt  23118  icomnfordt  23119  iooordt  23120  cnrest2  23189  cmpcov2  23293  fiuncmp  23307  bwth  23313  indisconn  23321  locfincmp  23429  xkococnlem  23562  hmphdis  23699  uzrest  23800  ufildr  23834  fin1aufil  23835  eltsms  24036  ustval  24106  qtopbaslem  24662  tgqioo  24704  re2ndc  24705  xrhmeo  24860  bndth  24873  pi1xfrcnvlem  24972  ovolficcss  25386  nulmbl2  25453  uniiccdif  25495  opnmbllem  25518  opnmblALT  25520  mbfimaopnlem  25572  i1fima  25595  i1fima2  25596  i1fd  25598  c1liplem1  25917  deg1n0ima  26010  efcvx  26375  dvrelog  26562  dvloglem  26573  logf1o2  26575  dvlog  26576  ressatans  26860  wilthlem3  26996  bday1s  27763  negsproplem2  27958  negsbdaylem  27985  onscutlt  28188  onsiso  28192  bdayon  28196  bdayn0p1  28281  trkgbas  28408  trkgdist  28409  trkgitv  28410  ex-ss  30389  ajfval  30771  ipasslem8  30799  hlimcaui  31198  shsspwh  31208  hhssabloi  31224  hhssnv  31226  hhshsslem1  31229  shunssji  31331  sshhococi  31508  pjoml6i  31551  osumcori  31605  mayete3i  31690  mayetes3i  31691  imaelshi  32020  pjclem1  32157  pjci  32162  mdcompli  32391  dmdcompli  32392  xppreima  32602  gsummpt2co  33014  cycpmrn  33098  elrgspnsubrunlem2  33198  evl1deg1  33521  evl1deg2  33522  evl1deg3  33523  circtopn  33803  esumpcvgval  34044  esumcvg  34052  ldgenpisyslem3  34131  elmbfmvol2  34234  sxbrsigalem0  34238  eulerpartlemsv3  34328  ballotlem7  34503  rpsqrtcn  34560  bnj931  34736  bnj1137  34961  subfacp1lem2a  35152  subfacp1lem2b  35153  erdszelem2  35164  kur14lem7  35184  kur14lem9  35186  dfon2lem2  35757  bj-snglsstag  36954  bj-2upln1upl  36997  bj-0int  37074  bj-opabssvv  37123  bj-ccssccbar  37190  bj-ccinftyssccbar  37191  bj-rvecsscvec  37277  icoreelrn  37334  finxpreclem3  37366  imadifss  37574  poimirlem4  37603  poimirlem26  37625  poimirlem27  37626  opnmbllem0  37635  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  volsupnfl  37644  sdclem2  37721  heibor1lem  37788  refrelsredund4  38608  dicval  41155  dvhdimlem  41423  ismrc  42674  mapfzcons1cl  42691  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  rabdiophlem2  42775  jm2.27dlem5  42986  algbase  43147  algaddg  43148  algmulr  43149  algsca  43150  algvsca  43151  intimass2  43628  comptiunov2i  43679  relexp0a  43689  lhe4.4ex1a  44302  iocnct  45522  iccnct  45523  dvcosre  45894  fourierdlem46  46134  fourierdlem57  46145  fourierdlem58  46146  fourierdlem62  46150  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem114  46202  sge0split  46391  sge0uzfsumgt  46426  hoiprodp1  46570  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  sbgoldbo  47772  usgrexmpl1lem  48006  usgrexmpl2lem  48011  dmmpossx2  48322  ipoglb0  48979  mreclat  48982  catbas  49212  cathomfval  49213  catcofval  49214  aacllem  49787