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

Syntax hints:   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  3sstr4i  3987  eqimss2i  3997  difsssymdif  4217  snsspr1  4772  snsspr2  4773  snsstp1  4774  snsstp2  4775  snsstp3  4776  unissint  4929  iunxdif2  5011  pwpwssunieq  5061  intabs  5296  inxpssres  5649  elopaelxp  5722  opabssxp  5724  dmresi  6019  cnvimass  6049  sofld  6153  cnvcnv  6158  cnvssrndm  6237  sssucid  6407  f1imadifssran  6586  cnvimainrn  7021  fvclss  7197  dmmpossx  8020  suppun  8136  frrlem12  8249  tfrlem11  8329  oawordeulem  8491  mapexOLD  8781  trcl  9649  djuunxp  9845  dfac3  10043  cfsuc  10179  isfin4p1  10237  fin23lem11  10239  domtriomlem  10364  ttukeylem1  10431  ttukeylem7  10437  brdom7disj  10453  brdom6disj  10454  fingch  10546  fpwwe2lem12  10565  canthp1lem2  10576  wunex2  10661  wunex3  10664  ressxr  11188  ltrelxr  11205  nnssnn0  12416  un0addcl  12446  un0mulcl  12447  nn0ssxnn0  12489  caubnd  15294  isumclim3  15694  iprodclim3  15935  bpoly4  15994  fprodefsum  16030  znnen  16149  isprm3  16622  phimullem  16718  isstruct2  17088  2strbas  17167  rngbase  17231  rngplusg  17232  rngmulr  17233  srngbase  17242  srngplusg  17243  srngmulr  17244  srnginvl  17245  lmodbase  17258  lmodplusg  17259  lmodsca  17260  lmodvsca  17261  ipsbase  17269  ipsaddg  17270  ipsmulr  17271  ipssca  17272  ipsvsca  17273  ipsip  17274  phlbase  17279  phlplusg  17280  phlsca  17281  phlvsca  17282  phlip  17283  topgrpbas  17294  topgrpplusg  17295  topgrptset  17296  otpsbas  17309  otpstset  17310  otpsle  17311  odrngbas  17336  odrngplusg  17337  odrngmulr  17338  odrngtset  17339  odrngle  17340  odrngds  17341  homarw  17982  ipoval  18465  ipolerval  18467  eqgfval  19117  cycsubg  19149  symgbas  19313  symgsubmefmndALT  19344  islbs3  21122  cnfldbas  21325  mpocnfldadd  21326  mpocnfldmul  21328  cnfldcj  21330  cnfldtset  21331  cnfldle  21332  cnfldds  21333  cnfldunif  21334  cnfldbasOLD  21340  cnfldaddOLD  21341  cnfldmulOLD  21342  cnfldcjOLD  21343  cnfldtsetOLD  21344  cnfldleOLD  21345  cnflddsOLD  21346  cnfldunifOLD  21347  basdif0  22909  iscldtop  23051  iocpnfordt  23171  icomnfordt  23172  iooordt  23173  cnrest2  23242  cmpcov2  23346  fiuncmp  23360  bwth  23366  indisconn  23374  locfincmp  23482  xkococnlem  23615  hmphdis  23752  uzrest  23853  ufildr  23887  fin1aufil  23888  eltsms  24089  ustval  24159  qtopbaslem  24714  tgqioo  24756  re2ndc  24757  xrhmeo  24912  bndth  24925  pi1xfrcnvlem  25024  ovolficcss  25438  nulmbl2  25505  uniiccdif  25547  opnmbllem  25570  opnmblALT  25572  mbfimaopnlem  25624  i1fima  25647  i1fima2  25648  i1fd  25650  c1liplem1  25969  deg1n0ima  26062  efcvx  26427  dvrelog  26614  dvloglem  26625  logf1o2  26627  dvlog  26628  ressatans  26912  wilthlem3  27048  bday1  27822  negsproplem2  28037  negbdaylem  28064  oncutlt  28272  oniso  28279  bdayons  28284  bdayn0p1  28377  trkgbas  28529  trkgdist  28530  trkgitv  28531  ex-ss  30514  ajfval  30896  ipasslem8  30924  hlimcaui  31323  shsspwh  31333  hhssabloi  31349  hhssnv  31351  hhshsslem1  31354  shunssji  31456  sshhococi  31633  pjoml6i  31676  osumcori  31730  mayete3i  31815  mayetes3i  31816  imaelshi  32145  pjclem1  32282  pjci  32287  mdcompli  32516  dmdcompli  32517  xppreima  32734  gsummpt2co  33141  cycpmrn  33236  elrgspnsubrunlem2  33341  evl1deg1  33668  evl1deg2  33669  evl1deg3  33670  circtopn  34014  esumpcvgval  34255  esumcvg  34263  ldgenpisyslem3  34342  elmbfmvol2  34444  sxbrsigalem0  34448  eulerpartlemsv3  34538  ballotlem7  34713  rpsqrtcn  34770  bnj931  34946  bnj1137  35170  fineqvnttrclse  35299  subfacp1lem2a  35393  subfacp1lem2b  35394  erdszelem2  35405  kur14lem7  35425  kur14lem9  35427  dfon2lem2  35995  regsfromunir1  36689  bj-snglsstag  37223  bj-2upln1upl  37266  bj-0int  37348  bj-opabssvv  37399  bj-ccssccbar  37466  bj-ccinftyssccbar  37467  bj-rvecsscvec  37553  icoreelrn  37610  finxpreclem3  37642  imadifss  37840  poimirlem4  37869  poimirlem26  37891  poimirlem27  37892  opnmbllem0  37901  mblfinlem3  37904  mblfinlem4  37905  ismblfin  37906  volsupnfl  37910  sdclem2  37987  heibor1lem  38054  refrelsredund4  38961  dicval  41546  dvhdimlem  41814  ismrc  43052  mapfzcons1cl  43069  2rexfrabdioph  43147  3rexfrabdioph  43148  4rexfrabdioph  43149  6rexfrabdioph  43150  7rexfrabdioph  43151  rabdiophlem2  43153  jm2.27dlem5  43364  algbase  43525  algaddg  43526  algmulr  43527  algsca  43528  algvsca  43529  intimass2  44005  comptiunov2i  44056  relexp0a  44066  lhe4.4ex1a  44679  iocnct  45894  iccnct  45895  dvcosre  46264  fourierdlem46  46504  fourierdlem57  46515  fourierdlem58  46516  fourierdlem62  46520  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem114  46572  sge0split  46761  sge0uzfsumgt  46796  hoiprodp1  46940  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  sbgoldbo  48141  usgrexmpl1lem  48375  usgrexmpl2lem  48380  dmmpossx2  48691  ipoglb0  49347  mreclat  49350  catbas  49579  cathomfval  49580  catcofval  49581  aacllem  50154