Theorem sseqtrri 3971

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

Syntax hints:   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  3sstr4i  3973  eqimss2i  3983  difsssymdif  4198  snsspr1  4752  snsspr2  4753  snsstp1  4754  snsstp2  4755  snsstp3  4756  unissint  4909  iunxdif2  4990  pwpwssunieq  5040  intabs  5284  inxpssres  5642  elopaelxp  5715  opabssxp  5717  dmresi  6011  cnvimass  6041  sofld  6145  cnvcnv  6150  cnvssrndm  6229  sssucid  6399  f1imadifssran  6578  cnvimainrn  7015  fvclss  7192  dmmpossx  8015  suppun  8131  frrlem12  8244  tfrlem11  8324  oawordeulem  8486  mapexOLD  8776  trcl  9647  djuunxp  9843  dfac3  10041  cfsuc  10177  isfin4p1  10235  fin23lem11  10237  domtriomlem  10362  ttukeylem1  10429  ttukeylem7  10435  brdom7disj  10451  brdom6disj  10452  fingch  10544  fpwwe2lem12  10563  canthp1lem2  10574  wunex2  10659  wunex3  10662  ressxr  11187  ltrelxr  11204  nnssnn0  12438  un0addcl  12468  un0mulcl  12469  nn0ssxnn0  12511  caubnd  15319  isumclim3  15719  iprodclim3  15963  bpoly4  16022  fprodefsum  16058  znnen  16177  isprm3  16650  phimullem  16747  isstruct2  17117  2strbas  17196  rngbase  17260  rngplusg  17261  rngmulr  17262  srngbase  17271  srngplusg  17272  srngmulr  17273  srnginvl  17274  lmodbase  17287  lmodplusg  17288  lmodsca  17289  lmodvsca  17290  ipsbase  17298  ipsaddg  17299  ipsmulr  17300  ipssca  17301  ipsvsca  17302  ipsip  17303  phlbase  17308  phlplusg  17309  phlsca  17310  phlvsca  17311  phlip  17312  topgrpbas  17323  topgrpplusg  17324  topgrptset  17325  otpsbas  17338  otpstset  17339  otpsle  17340  odrngbas  17365  odrngplusg  17366  odrngmulr  17367  odrngtset  17368  odrngle  17369  odrngds  17370  homarw  18011  ipoval  18494  ipolerval  18496  eqgfval  19149  cycsubg  19181  symgbas  19345  symgsubmefmndALT  19376  islbs3  21155  cnfldbas  21358  mpocnfldadd  21359  mpocnfldmul  21361  cnfldcj  21363  cnfldtset  21364  cnfldle  21365  cnfldds  21366  cnfldunif  21367  basdif0  22943  iscldtop  23085  iocpnfordt  23205  icomnfordt  23206  iooordt  23207  cnrest2  23276  cmpcov2  23380  fiuncmp  23394  bwth  23400  indisconn  23408  locfincmp  23516  xkococnlem  23649  hmphdis  23786  uzrest  23887  ufildr  23921  fin1aufil  23922  eltsms  24123  ustval  24193  qtopbaslem  24748  tgqioo  24790  re2ndc  24791  xrhmeo  24938  bndth  24950  pi1xfrcnvlem  25048  ovolficcss  25461  nulmbl2  25528  uniiccdif  25570  opnmbllem  25593  opnmblALT  25595  mbfimaopnlem  25647  i1fima  25670  i1fima2  25671  i1fd  25673  c1liplem1  25988  deg1n0ima  26079  efcvx  26439  dvrelog  26626  dvloglem  26637  logf1o2  26639  dvlog  26640  ressatans  26923  wilthlem3  27058  bday1  27831  negsproplem2  28046  negbdaylem  28073  oncutlt  28281  oniso  28288  bdayons  28293  bdayn0p1  28386  trkgbas  28538  trkgdist  28539  trkgitv  28540  ex-ss  30522  ajfval  30905  ipasslem8  30933  hlimcaui  31332  shsspwh  31342  hhssabloi  31358  hhssnv  31360  hhshsslem1  31363  shunssji  31465  sshhococi  31642  pjoml6i  31685  osumcori  31739  mayete3i  31824  mayetes3i  31825  imaelshi  32154  pjclem1  32291  pjci  32296  mdcompli  32525  dmdcompli  32526  xppreima  32744  gsummpt2co  33136  cycpmrn  33231  elrgspnsubrunlem2  33336  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  circtopn  34028  esumpcvgval  34269  esumcvg  34277  ldgenpisyslem3  34356  elmbfmvol2  34458  sxbrsigalem0  34462  eulerpartlemsv3  34552  ballotlem7  34727  rpsqrtcn  34784  bnj931  34960  bnj1137  35184  fineqvnttrclse  35312  subfacp1lem2a  35415  subfacp1lem2b  35416  erdszelem2  35427  kur14lem7  35447  kur14lem9  35449  dfon2lem2  36017  regsfromunir1  36775  bj-snglsstag  37341  bj-2upln1upl  37384  bj-0int  37466  bj-opabssvv  37517  bj-ccssccbar  37584  bj-ccinftyssccbar  37585  bj-rvecsscvec  37671  icoreelrn  37730  finxpreclem3  37762  imadifss  37969  poimirlem4  37998  poimirlem26  38020  poimirlem27  38021  opnmbllem0  38030  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  volsupnfl  38039  sdclem2  38116  heibor1lem  38183  refrelsredund4  39090  dicval  41675  dvhdimlem  41943  ismrc  43157  mapfzcons1cl  43174  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  rabdiophlem2  43254  jm2.27dlem5  43465  algbase  43626  algaddg  43627  algmulr  43628  algsca  43629  algvsca  43630  intimass2  44106  comptiunov2i  44157  relexp0a  44167  lhe4.4ex1a  44780  iocnct  45992  iccnct  45993  dvcosre  46362  fourierdlem46  46602  fourierdlem57  46613  fourierdlem58  46614  fourierdlem62  46618  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem114  46670  sge0split  46859  sge0uzfsumgt  46894  hoiprodp1  47038  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  sbgoldbo  48285  usgrexmpl1lem  48519  usgrexmpl2lem  48524  dmmpossx2  48835  ipoglb0  49491  mreclat  49494  catbas  49723  cathomfval  49724  catcofval  49725  aacllem  50298