Theorem sseqtrri 3989

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  3sstr4i  3991  eqimss2i  4001  difsssymdif  4219  snsspr1  4785  snsspr2  4786  snsstp1  4787  snsstp2  4788  snsstp3  4789  unissint  4942  iunxdif2  5023  pwpwssunieq  5075  intabs  5324  inxpssres  5683  elopaelxp  5756  opabssxp  5758  dmresi  6059  cnvimass  6089  sofld  6190  cnvcnv  6195  imadifssran  6207  cnvssrndm  6278  sssucid  6450  cnvimainrn  7069  fvclss  7246  dmmpossx  8072  suppun  8189  frrlem12  8303  tfrlem11  8384  oawordeulem  8548  trcl  9707  djuunxp  9926  dfac3  10124  cfsuc  10259  isfin4p1  10317  fin23lem11  10319  domtriomlem  10444  ttukeylem1  10511  ttukeylem7  10517  brdom7disj  10533  brdom6disj  10534  fingch  10626  fpwwe2lem12  10645  canthp1lem2  10656  wunex2  10741  wunex3  10744  ressxr  11271  ltrelxr  11288  nnssnn0  12525  un0addcl  12555  un0mulcl  12556  nn0ssxnn0  12598  caubnd  15436  isumclim3  15836  iprodclim3  16080  bpoly4  16138  fprodefsum  16174  znnen  16293  isprm3  16766  phimullem  16863  isstruct2  17234  2strbas  17313  rngbase  17377  rngplusg  17378  rngmulr  17379  srngbase  17388  srngplusg  17389  srngmulr  17390  srnginvl  17391  lmodbase  17404  lmodplusg  17405  lmodsca  17406  lmodvsca  17407  ipsbase  17415  ipsaddg  17416  ipsmulr  17417  ipssca  17418  ipsvsca  17419  ipsip  17420  phlbase  17425  phlplusg  17426  phlsca  17427  phlvsca  17428  phlip  17429  topgrpbas  17440  topgrpplusg  17441  topgrptset  17442  otpsbas  17455  otpstset  17456  otpsle  17457  odrngbas  17482  odrngplusg  17483  odrngmulr  17484  odrngtset  17485  odrngle  17486  odrngds  17487  homarw  18128  ipoval  18611  ipolerval  18613  eqgfval  19275  cycsubg  19310  symgbas  19473  symgsubmefmndALT  19504  islbs3  21316  cnfldbas  21563  mpocnfldadd  21564  mpocnfldmul  21566  cnfldcj  21568  cnfldtset  21569  cnfldle  21570  cnfldds  21571  cnfldunif  21572  basdif0  23147  iscldtop  23289  iocpnfordt  23409  icomnfordt  23410  iooordt  23411  cnrest2  23480  cmpcov2  23584  fiuncmp  23598  bwth  23604  indisconn  23612  locfincmp  23720  xkococnlem  23853  hmphdis  23990  uzrest  24091  ufildr  24125  fin1aufil  24126  eltsms  24327  ustval  24397  qtopbaslem  24952  tgqioo  24994  re2ndc  24995  xrhmeo  25142  bndth  25154  pi1xfrcnvlem  25252  ovolficcss  25665  nulmbl2  25732  uniiccdif  25774  opnmbllem  25797  opnmblALT  25799  mbfimaopnlem  25851  i1fima  25874  i1fima2  25875  i1fd  25877  c1liplem1  26192  deg1n0ima  26283  efcvx  26649  dvrelog  26839  dvloglem  26850  logf1o2  26852  dvlog  26853  ressatans  27136  wilthlem3  27271  bday1  28044  negsproplem2  28259  negbdaylem  28286  oncutlt  28494  oniso  28501  bdayons  28506  bdayn0p1  28599  trkgbas  28751  trkgdist  28752  trkgitv  28753  ex-ss  30815  ajfval  31198  ipasslem8  31226  hlimcaui  31625  shsspwh  31635  hhssabloi  31651  hhssnv  31653  hhshsslem1  31656  shunssji  31758  sshhococi  31935  pjoml6i  31978  osumcori  32032  mayete3i  32117  mayetes3i  32118  imaelshi  32447  pjclem1  32584  pjci  32589  mdcompli  32818  dmdcompli  32819  xppreima  33027  gsummpt2co  33399  cycpmrn  33494  elrgspnsubrunlem2  33599  evl1deg1  33897  evl1deg2  33898  evl1deg3  33899  circtopn  34258  esumpcvgval  34499  esumcvg  34507  ldgenpisyslem3  34587  elmbfmvol2  34689  sxbrsigalem0  34693  eulerpartlemsv3  34783  ballotlem7  34958  rpsqrtcn  35012  bnj931  35191  bnj1137  35415  fineqvnttrclse  35561  subfacp1lem2a  35693  subfacp1lem2b  35694  erdszelem2  35705  kur14lem7  35725  kur14lem9  35727  dfon2lem2  36295  regsfromunir1  37092  bj-snglsstag  37658  bj-2upln1upl  37701  bj-0int  37784  bj-opabssvv  37835  bj-ccssccbar  37902  bj-ccinftyssccbar  37903  bj-rvecsscvec  37989  icoreelrn  38048  finxpreclem3  38080  imadifss  38287  poimirlem4  38316  poimirlem26  38338  poimirlem27  38339  opnmbllem0  38348  mblfinlem3  38351  mblfinlem4  38352  ismblfin  38353  volsupnfl  38357  sdclem2  38434  heibor1lem  38501  refrelsredund4  39406  dicval  41991  dvhdimlem  42259  ismrc  43473  mapfzcons1cl  43490  2rexfrabdioph  43564  3rexfrabdioph  43565  4rexfrabdioph  43566  6rexfrabdioph  43567  7rexfrabdioph  43568  rabdiophlem2  43570  jm2.27dlem5  43781  algbase  43942  algaddg  43943  algmulr  43944  algsca  43945  algvsca  43946  intimass2  44422  comptiunov2i  44473  relexp0a  44483  lhe4.4ex1a  45080  iocnct  46297  iccnct  46298  dvcosre  46667  fourierdlem46  46907  fourierdlem57  46918  fourierdlem58  46919  fourierdlem62  46923  fourierdlem102  46963  fourierdlem103  46964  fourierdlem104  46965  fourierdlem114  46975  sge0split  47164  sge0uzfsumgt  47199  hoiprodp1  47343  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  sbgoldbo  48593  usgrexmpl1lem  48827  usgrexmpl2lem  48832  dmmpossx2  49158  ipoglb0  49813  mreclat  49816  catbas  50045  cathomfval  50046  catcofval  50047  aacllem  50662