Theorem sseqtrri 4019

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

Syntax hints:   = wceq 1533   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  eqimss2i  4043  difsssymdif  4255  snsspr1  4822  snsspr2  4823  snsstp1  4824  snsstp2  4825  snsstp3  4826  unissint  4979  iunxdif2  5060  pwpwssunieq  5111  intabs  5348  inxpssres  5699  elopaelxp  5771  opabssxp  5774  dmresi  6060  cnvimass  6090  sofld  6196  cnvcnv  6201  cnvssrndm  6280  sssucid  6454  cnvimainrn  7081  fvclss  7257  dmmpossx  8076  suppun  8195  frrlem12  8309  wfrlem14OLD  8349  tfrlem11  8415  oawordeulem  8581  mapex  8857  trcl  9759  djuunxp  9952  dfac3  10152  cfsuc  10288  isfin4p1  10346  fin23lem11  10348  domtriomlem  10473  ttukeylem1  10540  ttukeylem7  10546  brdom7disj  10562  brdom6disj  10563  fingch  10654  fpwwe2lem12  10673  canthp1lem2  10684  wunex2  10769  wunex3  10772  ressxr  11296  ltrelxr  11313  nnssnn0  12513  un0addcl  12543  un0mulcl  12544  nn0ssxnn0  12585  caubnd  15345  isumclim3  15745  iprodclim3  15984  bpoly4  16043  fprodefsum  16079  znnen  16196  isprm3  16661  phimullem  16755  isstruct2  17125  2strbas  17210  2strop  17211  2strbas1  17214  rngbase  17287  rngplusg  17288  rngmulr  17289  srngbase  17298  srngplusg  17299  srngmulr  17300  srnginvl  17301  lmodbase  17314  lmodplusg  17315  lmodsca  17316  lmodvsca  17317  ipsbase  17325  ipsaddg  17326  ipsmulr  17327  ipssca  17328  ipsvsca  17329  ipsip  17330  phlbase  17335  phlplusg  17336  phlsca  17337  phlvsca  17338  phlip  17339  topgrpbas  17350  topgrpplusg  17351  topgrptset  17352  otpsbas  17365  otpstset  17366  otpsle  17367  odrngbas  17392  odrngplusg  17393  odrngmulr  17394  odrngtset  17395  odrngle  17396  odrngds  17397  homarw  18042  ipoval  18529  ipolerval  18531  eqgfval  19138  cycsubg  19170  symgbas  19332  symgsubmefmndALT  19365  islbs3  21050  cnfldbas  21290  mpocnfldadd  21291  mpocnfldmul  21293  cnfldcj  21295  cnfldtset  21296  cnfldle  21297  cnfldds  21298  cnfldunif  21299  cnfldbasOLD  21305  cnfldaddOLD  21306  cnfldmulOLD  21307  cnfldcjOLD  21308  cnfldtsetOLD  21309  cnfldleOLD  21310  cnflddsOLD  21311  cnfldunifOLD  21312  basdif0  22876  iscldtop  23019  iocpnfordt  23139  icomnfordt  23140  iooordt  23141  cnrest2  23210  cmpcov2  23314  fiuncmp  23328  bwth  23334  indisconn  23342  locfincmp  23450  xkococnlem  23583  hmphdis  23720  uzrest  23821  ufildr  23855  fin1aufil  23856  eltsms  24057  ustval  24127  qtopbaslem  24695  tgqioo  24736  re2ndc  24737  xrhmeo  24891  bndth  24904  pi1xfrcnvlem  25003  ovolficcss  25418  nulmbl2  25485  uniiccdif  25527  opnmbllem  25550  opnmblALT  25552  mbfimaopnlem  25604  i1fima  25627  i1fima2  25628  i1fd  25630  c1liplem1  25949  deg1n0ima  26045  efcvx  26406  dvrelog  26591  dvloglem  26602  logf1o2  26604  dvlog  26605  ressatans  26886  wilthlem3  27022  bday1s  27784  negsproplem2  27961  negsbdaylem  27988  trkgbas  28269  trkgdist  28270  trkgitv  28271  ex-ss  30257  ajfval  30639  ipasslem8  30667  hlimcaui  31066  shsspwh  31076  hhssabloi  31092  hhssnv  31094  hhshsslem1  31097  shunssji  31199  sshhococi  31376  pjoml6i  31419  osumcori  31473  mayete3i  31558  mayetes3i  31559  imaelshi  31888  pjclem1  32025  pjci  32030  mdcompli  32259  dmdcompli  32260  xppreima  32453  gsummpt2co  32783  cycpmrn  32885  circtopn  33471  esumpcvgval  33730  esumcvg  33738  ldgenpisyslem3  33817  elmbfmvol2  33920  sxbrsigalem0  33924  eulerpartlemsv3  34014  ballotlem7  34188  rpsqrtcn  34258  bnj931  34434  bnj1137  34659  subfacp1lem2a  34823  subfacp1lem2b  34824  erdszelem2  34835  kur14lem7  34855  kur14lem9  34857  dfon2lem2  35413  bj-snglsstag  36493  bj-2upln1upl  36536  bj-0int  36613  bj-opabssvv  36662  bj-ccssccbar  36729  bj-ccinftyssccbar  36730  bj-rvecsscvec  36816  icoreelrn  36873  finxpreclem3  36905  imadifss  37101  poimirlem4  37130  poimirlem26  37152  poimirlem27  37153  opnmbllem0  37162  mblfinlem3  37165  mblfinlem4  37166  ismblfin  37167  volsupnfl  37171  sdclem2  37248  heibor1lem  37315  refrelsredund4  38136  dicval  40681  dvhdimlem  40949  ismrc  42152  mapfzcons1cl  42169  2rexfrabdioph  42247  3rexfrabdioph  42248  4rexfrabdioph  42249  6rexfrabdioph  42250  7rexfrabdioph  42251  rabdiophlem2  42253  jm2.27dlem5  42465  algbase  42633  algaddg  42634  algmulr  42635  algsca  42636  algvsca  42637  intimass2  43116  comptiunov2i  43167  relexp0a  43177  lhe4.4ex1a  43797  iocnct  44954  iccnct  44955  dvcosre  45329  fourierdlem46  45569  fourierdlem57  45580  fourierdlem58  45581  fourierdlem62  45585  fourierdlem102  45625  fourierdlem103  45626  fourierdlem104  45627  fourierdlem114  45637  sge0split  45826  sge0uzfsumgt  45861  hoiprodp1  46005  hoidmvlelem1  46012  hoidmvlelem2  46013  hoidmvlelem3  46014  sbgoldbo  47156  dmmpossx2  47478  ipoglb0  48083  mreclat  48086  aacllem  48312