Theorem sseqtrri 3962

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3sstr4i  3964  eqimss2i  3974  difsssymdif  4211  snsspr1  4773  snsspr2  4774  snsstp1  4775  snsstp2  4776  snsstp3  4777  unissint  4935  iunxdif2  5015  pwpwssunieq  5067  intabs  5314  inxpssres  5672  elopaelxp  5746  opabssxp  5748  relopabi  5805  dmresi  6056  sofld  6191  cnvcnv  6196  imassrn  6210  cnvimass  6211  imadifssranOLD  6215  cnvssrndm  6291  sssucid  6463  cnvimainrn  7090  fvclss  7268  dmmpossx  8102  suppun  8229  frrlem12  8343  tfrlem11  8424  oawordeulem  8590  trcl  9756  djuunxp  10029  dfac3  10227  cfsuc  10362  isfin4p1  10420  fin23lem11  10422  domtriomlem  10547  ttukeylem1  10614  ttukeylem7  10620  brdom7disj  10637  brdom6disj  10638  fingch  10735  fpwwe2lem12  10754  canthp1lem2  10765  wunex2  10850  wunex3  10853  ressxr  11380  ltrelxr  11397  nnssnn0  12636  un0addcl  12666  un0mulcl  12667  nn0ssxnn0  12709  caubnd  15555  isumclim3  15954  iprodclim3  16196  bpoly4  16254  fprodefsum  16290  znnen  16409  isprm3  16887  phimullem  16985  isstruct2  17356  2strbas  17435  rngbase  17499  rngplusg  17500  rngmulr  17501  srngbase  17510  srngplusg  17511  srngmulr  17512  srnginvl  17513  lmodbase  17526  lmodplusg  17527  lmodsca  17528  lmodvsca  17529  ipsbase  17537  ipsaddg  17538  ipsmulr  17539  ipssca  17540  ipsvsca  17541  ipsip  17542  phlbase  17547  phlplusg  17548  phlsca  17549  phlvsca  17550  phlip  17551  topgrpbas  17562  topgrpplusg  17563  topgrptset  17564  otpsbas  17577  otpstset  17578  otpsle  17579  odrngbas  17604  odrngplusg  17605  odrngmulr  17606  odrngtset  17607  odrngle  17608  odrngds  17609  homarw  18250  ipoval  18733  ipolerval  18735  eqgfval  19417  cycsubg  19452  symgbas  19616  symgsubmefmndALT  19647  islbs3  21463  cnfldbas  21712  mpocnfldadd  21713  mpocnfldmul  21715  cnfldcj  21717  cnfldtset  21718  cnfldle  21719  cnfldds  21720  cnfldunif  21721  basdif0  23301  iscldtop  23443  iocpnfordt  23563  icomnfordt  23564  iooordt  23565  cnrest2  23634  cmpcov2  23738  fiuncmp  23752  bwth  23758  indisconn  23766  locfincmp  23875  xkococnlem  24008  hmphdis  24145  uzrest  24246  ufildr  24280  fin1aufil  24281  eltsms  24482  ustval  24552  qtopbaslem  25107  tgqioo  25149  re2ndc  25150  xrhmeo  25297  bndth  25309  pi1xfrcnvlem  25407  ovolficcss  25820  nulmbl2  25887  uniiccdif  25929  opnmbllem  25952  opnmblALT  25954  mbfimaopnlem  26006  i1fima  26029  i1fima2  26030  i1fd  26032  c1liplem1  26346  deg1n0ima  26437  efcvx  26806  dvrelog  26995  dvloglem  27006  logf1o2  27008  dvlog  27009  ressatans  27292  wilthlem3  27427  bday1  28230  negsproplem2  28445  negbdaylem  28472  oncutlt  28680  oniso  28687  bdayons  28692  bdayn0p1  28785  trkgbas  28937  trkgdist  28938  trkgitv  28939  ex-ss  31058  ajfval  31441  ipasslem8  31469  hlimcaui  31868  shsspwh  31878  hhssabloi  31894  hhssnv  31896  hhshsslem1  31899  shunssji  32001  sshhococi  32178  pjoml6i  32221  osumcori  32275  mayete3i  32360  mayetes3i  32361  imaelshi  32690  pjclem1  32827  pjci  32832  mdcompli  33061  dmdcompli  33062  xppreima  33311  gsummpt2co  33679  cycpmrn  33774  elrgspnsubrunlem2  33879  evl1deg1  34178  evl1deg2  34179  evl1deg3  34180  circtopn  34539  esumpcvgval  34780  esumcvg  34788  ldgenpisyslem3  34868  elmbfmvol2  34969  sxbrsigalem0  34973  eulerpartlemsv3  35063  ballotlem7  35238  rpsqrtcn  35292  bnj931  35471  bnj1137  35695  fineqvnttrclse  35892  jf1o  36011  subfacp1lem2a  36112  subfacp1lem2b  36113  erdszelem2  36124  kur14lem7  36144  kur14lem9  36146  dfon2lem2  36724  regsfromunir1  37506  bj-snglsstag  38072  bj-2upln1upl  38115  bj-0int  38213  bj-opabssvv  38263  bj-ccssccbar  38330  bj-ccinftyssccbar  38331  bj-rvecsscvec  38417  icoreelrn  38476  finxpreclem3  38508  imadifss  38715  poimirlem4  38734  poimirlem26  38756  poimirlem27  38757  opnmbllem0  38766  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  volsupnfl  38775  sdclem2  38868  heibor1lem  38935  refrelsredund4  39840  dicval  42425  dvhdimlem  42693  ismrc  43905  mapfzcons1cl  43922  2rexfrabdioph  43996  3rexfrabdioph  43997  4rexfrabdioph  43998  6rexfrabdioph  43999  7rexfrabdioph  44000  rabdiophlem2  44002  jm2.27dlem5  44213  algbase  44368  algaddg  44369  algmulr  44370  algsca  44371  algvsca  44372  intimass2  44847  comptiunov2i  44898  relexp0a  44908  lhe4.4ex1a  45505  iocnct  46757  iccnct  46758  dvcosre  47127  fourierdlem46  47367  fourierdlem57  47378  fourierdlem58  47379  fourierdlem62  47383  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem114  47435  sge0split  47624  sge0uzfsumgt  47659  hoiprodp1  47803  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem3  47812  sbgoldbo  49090  usgrexmpl1lem  49324  usgrexmpl2lem  49329  dmmpossx2  49654  ipoglb0  50313  mreclat  50316  catbas  50553  cathomfval  50554  catcofval  50555  parhomssun  50952  aacllem  51219