Theorem sseqtrri 3985

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

Syntax hints:   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  3sstr4i  3987  eqimss2i  3997  difsssymdif  4215  snsspr1  4771  snsspr2  4772  snsstp1  4773  snsstp2  4774  snsstp3  4775  unissint  4929  iunxdif2  5010  pwpwssunieq  5060  intabs  5304  inxpssres  5662  elopaelxp  5735  opabssxp  5737  dmresi  6038  cnvimass  6068  sofld  6169  cnvcnv  6174  cnvssrndm  6254  sssucid  6424  f1imadifssran  6603  cnvimainrn  7044  fvclss  7221  dmmpossx  8043  suppun  8159  frrlem12  8273  tfrlem11  8354  oawordeulem  8518  mapexOLD  8809  trcl  9680  djuunxp  9876  dfac3  10074  cfsuc  10211  isfin4p1  10269  fin23lem11  10271  domtriomlem  10396  ttukeylem1  10463  ttukeylem7  10469  brdom7disj  10485  brdom6disj  10486  fingch  10578  fpwwe2lem12  10597  canthp1lem2  10608  wunex2  10693  wunex3  10696  ressxr  11223  ltrelxr  11240  nnssnn0  12481  un0addcl  12511  un0mulcl  12512  nn0ssxnn0  12554  caubnd  15369  isumclim3  15769  iprodclim3  16013  bpoly4  16072  fprodefsum  16108  znnen  16227  isprm3  16700  phimullem  16797  isstruct2  17168  2strbas  17247  rngbase  17311  rngplusg  17312  rngmulr  17313  srngbase  17322  srngplusg  17323  srngmulr  17324  srnginvl  17325  lmodbase  17338  lmodplusg  17339  lmodsca  17340  lmodvsca  17341  ipsbase  17349  ipsaddg  17350  ipsmulr  17351  ipssca  17352  ipsvsca  17353  ipsip  17354  phlbase  17359  phlplusg  17360  phlsca  17361  phlvsca  17362  phlip  17363  topgrpbas  17374  topgrpplusg  17375  topgrptset  17376  otpsbas  17389  otpstset  17390  otpsle  17391  odrngbas  17416  odrngplusg  17417  odrngmulr  17418  odrngtset  17419  odrngle  17420  odrngds  17421  homarw  18062  ipoval  18545  ipolerval  18547  eqgfval  19200  cycsubg  19232  symgbas  19395  symgsubmefmndALT  19426  islbs3  21205  cnfldbas  21408  mpocnfldadd  21409  mpocnfldmul  21411  cnfldcj  21413  cnfldtset  21414  cnfldle  21415  cnfldds  21416  cnfldunif  21417  basdif0  22993  iscldtop  23135  iocpnfordt  23255  icomnfordt  23256  iooordt  23257  cnrest2  23326  cmpcov2  23430  fiuncmp  23444  bwth  23450  indisconn  23458  locfincmp  23566  xkococnlem  23699  hmphdis  23836  uzrest  23937  ufildr  23971  fin1aufil  23972  eltsms  24173  ustval  24243  qtopbaslem  24798  tgqioo  24840  re2ndc  24841  xrhmeo  24988  bndth  25000  pi1xfrcnvlem  25098  ovolficcss  25511  nulmbl2  25578  uniiccdif  25620  opnmbllem  25643  opnmblALT  25645  mbfimaopnlem  25697  i1fima  25720  i1fima2  25721  i1fd  25723  c1liplem1  26038  deg1n0ima  26129  efcvx  26489  dvrelog  26679  dvloglem  26690  logf1o2  26692  dvlog  26693  ressatans  26976  wilthlem3  27111  bday1  27884  negsproplem2  28099  negbdaylem  28126  oncutlt  28334  oniso  28341  bdayons  28346  bdayn0p1  28439  trkgbas  28591  trkgdist  28592  trkgitv  28593  ex-ss  30575  ajfval  30958  ipasslem8  30986  hlimcaui  31385  shsspwh  31395  hhssabloi  31411  hhssnv  31413  hhshsslem1  31416  shunssji  31518  sshhococi  31695  pjoml6i  31738  osumcori  31792  mayete3i  31877  mayetes3i  31878  imaelshi  32207  pjclem1  32344  pjci  32349  mdcompli  32578  dmdcompli  32579  xppreima  32797  gsummpt2co  33189  cycpmrn  33284  elrgspnsubrunlem2  33390  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  circtopn  34095  esumpcvgval  34336  esumcvg  34344  ldgenpisyslem3  34423  elmbfmvol2  34525  sxbrsigalem0  34529  eulerpartlemsv3  34619  ballotlem7  34794  rpsqrtcn  34851  bnj931  35030  bnj1137  35254  fineqvnttrclse  35384  subfacp1lem2a  35494  subfacp1lem2b  35495  erdszelem2  35506  kur14lem7  35526  kur14lem9  35528  dfon2lem2  36096  regsfromunir1  36864  bj-snglsstag  37430  bj-2upln1upl  37473  bj-0int  37555  bj-opabssvv  37606  bj-ccssccbar  37673  bj-ccinftyssccbar  37674  bj-rvecsscvec  37760  icoreelrn  37819  finxpreclem3  37851  imadifss  38058  poimirlem4  38087  poimirlem26  38109  poimirlem27  38110  opnmbllem0  38119  mblfinlem3  38122  mblfinlem4  38123  ismblfin  38124  volsupnfl  38128  sdclem2  38205  heibor1lem  38272  refrelsredund4  39179  dicval  41764  dvhdimlem  42032  ismrc  43246  mapfzcons1cl  43263  2rexfrabdioph  43337  3rexfrabdioph  43338  4rexfrabdioph  43339  6rexfrabdioph  43340  7rexfrabdioph  43341  rabdiophlem2  43343  jm2.27dlem5  43554  algbase  43715  algaddg  43716  algmulr  43717  algsca  43718  algvsca  43719  intimass2  44195  comptiunov2i  44246  relexp0a  44256  lhe4.4ex1a  44869  iocnct  46080  iccnct  46081  dvcosre  46450  fourierdlem46  46690  fourierdlem57  46701  fourierdlem58  46702  fourierdlem62  46706  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem114  46758  sge0split  46947  sge0uzfsumgt  46982  hoiprodp1  47126  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  sbgoldbo  48373  usgrexmpl1lem  48607  usgrexmpl2lem  48612  dmmpossx2  48923  ipoglb0  49579  mreclat  49582  catbas  49811  cathomfval  49812  catcofval  49813  aacllem  50386