Theorem sseqtrri 3999

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

Syntax hints:   = wceq 1540   ⊆ wss 3917

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 2702

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

This theorem is referenced by:  3sstr4i  4001  eqimss2i  4011  difsssymdif  4229  snsspr1  4781  snsspr2  4782  snsstp1  4783  snsstp2  4784  snsstp3  4785  unissint  4939  iunxdif2  5020  pwpwssunieq  5071  intabs  5307  inxpssres  5658  elopaelxp  5731  opabssxp  5734  dmresi  6026  cnvimass  6056  sofld  6163  cnvcnv  6168  cnvssrndm  6247  sssucid  6417  f1imadifssran  6605  cnvimainrn  7042  fvclss  7218  dmmpossx  8048  suppun  8166  frrlem12  8279  tfrlem11  8359  oawordeulem  8521  mapexOLD  8808  trcl  9688  djuunxp  9881  dfac3  10081  cfsuc  10217  isfin4p1  10275  fin23lem11  10277  domtriomlem  10402  ttukeylem1  10469  ttukeylem7  10475  brdom7disj  10491  brdom6disj  10492  fingch  10583  fpwwe2lem12  10602  canthp1lem2  10613  wunex2  10698  wunex3  10701  ressxr  11225  ltrelxr  11242  nnssnn0  12452  un0addcl  12482  un0mulcl  12483  nn0ssxnn0  12525  caubnd  15332  isumclim3  15732  iprodclim3  15973  bpoly4  16032  fprodefsum  16068  znnen  16187  isprm3  16660  phimullem  16756  isstruct2  17126  2strbas  17205  rngbase  17269  rngplusg  17270  rngmulr  17271  srngbase  17280  srngplusg  17281  srngmulr  17282  srnginvl  17283  lmodbase  17296  lmodplusg  17297  lmodsca  17298  lmodvsca  17299  ipsbase  17307  ipsaddg  17308  ipsmulr  17309  ipssca  17310  ipsvsca  17311  ipsip  17312  phlbase  17317  phlplusg  17318  phlsca  17319  phlvsca  17320  phlip  17321  topgrpbas  17332  topgrpplusg  17333  topgrptset  17334  otpsbas  17347  otpstset  17348  otpsle  17349  odrngbas  17374  odrngplusg  17375  odrngmulr  17376  odrngtset  17377  odrngle  17378  odrngds  17379  homarw  18015  ipoval  18496  ipolerval  18498  eqgfval  19115  cycsubg  19147  symgbas  19309  symgsubmefmndALT  19340  islbs3  21072  cnfldbas  21275  mpocnfldadd  21276  mpocnfldmul  21278  cnfldcj  21280  cnfldtset  21281  cnfldle  21282  cnfldds  21283  cnfldunif  21284  cnfldbasOLD  21290  cnfldaddOLD  21291  cnfldmulOLD  21292  cnfldcjOLD  21293  cnfldtsetOLD  21294  cnfldleOLD  21295  cnflddsOLD  21296  cnfldunifOLD  21297  basdif0  22847  iscldtop  22989  iocpnfordt  23109  icomnfordt  23110  iooordt  23111  cnrest2  23180  cmpcov2  23284  fiuncmp  23298  bwth  23304  indisconn  23312  locfincmp  23420  xkococnlem  23553  hmphdis  23690  uzrest  23791  ufildr  23825  fin1aufil  23826  eltsms  24027  ustval  24097  qtopbaslem  24653  tgqioo  24695  re2ndc  24696  xrhmeo  24851  bndth  24864  pi1xfrcnvlem  24963  ovolficcss  25377  nulmbl2  25444  uniiccdif  25486  opnmbllem  25509  opnmblALT  25511  mbfimaopnlem  25563  i1fima  25586  i1fima2  25587  i1fd  25589  c1liplem1  25908  deg1n0ima  26001  efcvx  26366  dvrelog  26553  dvloglem  26564  logf1o2  26566  dvlog  26567  ressatans  26851  wilthlem3  26987  bday1s  27750  negsproplem2  27942  negsbdaylem  27969  onscutlt  28172  onsiso  28176  bdayon  28180  bdayn0p1  28265  trkgbas  28379  trkgdist  28380  trkgitv  28381  ex-ss  30363  ajfval  30745  ipasslem8  30773  hlimcaui  31172  shsspwh  31182  hhssabloi  31198  hhssnv  31200  hhshsslem1  31203  shunssji  31305  sshhococi  31482  pjoml6i  31525  osumcori  31579  mayete3i  31664  mayetes3i  31665  imaelshi  31994  pjclem1  32131  pjci  32136  mdcompli  32365  dmdcompli  32366  xppreima  32576  gsummpt2co  32995  cycpmrn  33107  elrgspnsubrunlem2  33206  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  circtopn  33834  esumpcvgval  34075  esumcvg  34083  ldgenpisyslem3  34162  elmbfmvol2  34265  sxbrsigalem0  34269  eulerpartlemsv3  34359  ballotlem7  34534  rpsqrtcn  34591  bnj931  34767  bnj1137  34992  subfacp1lem2a  35174  subfacp1lem2b  35175  erdszelem2  35186  kur14lem7  35206  kur14lem9  35208  dfon2lem2  35779  bj-snglsstag  36976  bj-2upln1upl  37019  bj-0int  37096  bj-opabssvv  37145  bj-ccssccbar  37212  bj-ccinftyssccbar  37213  bj-rvecsscvec  37299  icoreelrn  37356  finxpreclem3  37388  imadifss  37596  poimirlem4  37625  poimirlem26  37647  poimirlem27  37648  opnmbllem0  37657  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  volsupnfl  37666  sdclem2  37743  heibor1lem  37810  refrelsredund4  38630  dicval  41177  dvhdimlem  41445  ismrc  42696  mapfzcons1cl  42713  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  rabdiophlem2  42797  jm2.27dlem5  43009  algbase  43170  algaddg  43171  algmulr  43172  algsca  43173  algvsca  43174  intimass2  43651  comptiunov2i  43702  relexp0a  43712  lhe4.4ex1a  44325  iocnct  45545  iccnct  45546  dvcosre  45917  fourierdlem46  46157  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  sge0split  46414  sge0uzfsumgt  46449  hoiprodp1  46593  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  sbgoldbo  47792  usgrexmpl1lem  48016  usgrexmpl2lem  48021  dmmpossx2  48329  ipoglb0  48986  mreclat  48989  catbas  49219  cathomfval  49220  catcofval  49221  aacllem  49794