Theorem sseqtrri 3972

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 3971	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1542   ⊆ wss 3890

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 3907

This theorem is referenced by:  3sstr4i  3974  eqimss2i  3984  difsssymdif  4204  snsspr1  4758  snsspr2  4759  snsstp1  4760  snsstp2  4761  snsstp3  4762  unissint  4915  iunxdif2  4997  pwpwssunieq  5047  intabs  5284  inxpssres  5639  elopaelxp  5712  opabssxp  5714  dmresi  6009  cnvimass  6039  sofld  6143  cnvcnv  6148  cnvssrndm  6227  sssucid  6397  f1imadifssran  6576  cnvimainrn  7011  fvclss  7187  dmmpossx  8010  suppun  8125  frrlem12  8238  tfrlem11  8318  oawordeulem  8480  mapexOLD  8770  trcl  9638  djuunxp  9834  dfac3  10032  cfsuc  10168  isfin4p1  10226  fin23lem11  10228  domtriomlem  10353  ttukeylem1  10420  ttukeylem7  10426  brdom7disj  10442  brdom6disj  10443  fingch  10535  fpwwe2lem12  10554  canthp1lem2  10565  wunex2  10650  wunex3  10653  ressxr  11177  ltrelxr  11194  nnssnn0  12405  un0addcl  12435  un0mulcl  12436  nn0ssxnn0  12478  caubnd  15283  isumclim3  15683  iprodclim3  15924  bpoly4  15983  fprodefsum  16019  znnen  16138  isprm3  16611  phimullem  16707  isstruct2  17077  2strbas  17156  rngbase  17220  rngplusg  17221  rngmulr  17222  srngbase  17231  srngplusg  17232  srngmulr  17233  srnginvl  17234  lmodbase  17247  lmodplusg  17248  lmodsca  17249  lmodvsca  17250  ipsbase  17258  ipsaddg  17259  ipsmulr  17260  ipssca  17261  ipsvsca  17262  ipsip  17263  phlbase  17268  phlplusg  17269  phlsca  17270  phlvsca  17271  phlip  17272  topgrpbas  17283  topgrpplusg  17284  topgrptset  17285  otpsbas  17298  otpstset  17299  otpsle  17300  odrngbas  17325  odrngplusg  17326  odrngmulr  17327  odrngtset  17328  odrngle  17329  odrngds  17330  homarw  17971  ipoval  18454  ipolerval  18456  eqgfval  19109  cycsubg  19141  symgbas  19305  symgsubmefmndALT  19336  islbs3  21112  cnfldbas  21315  mpocnfldadd  21316  mpocnfldmul  21318  cnfldcj  21320  cnfldtset  21321  cnfldle  21322  cnfldds  21323  cnfldunif  21324  cnfldbasOLD  21330  cnfldaddOLD  21331  cnfldmulOLD  21332  cnfldcjOLD  21333  cnfldtsetOLD  21334  cnfldleOLD  21335  cnflddsOLD  21336  cnfldunifOLD  21337  basdif0  22896  iscldtop  23038  iocpnfordt  23158  icomnfordt  23159  iooordt  23160  cnrest2  23229  cmpcov2  23333  fiuncmp  23347  bwth  23353  indisconn  23361  locfincmp  23469  xkococnlem  23602  hmphdis  23739  uzrest  23840  ufildr  23874  fin1aufil  23875  eltsms  24076  ustval  24146  qtopbaslem  24701  tgqioo  24743  re2ndc  24744  xrhmeo  24891  bndth  24903  pi1xfrcnvlem  25001  ovolficcss  25414  nulmbl2  25481  uniiccdif  25523  opnmbllem  25546  opnmblALT  25548  mbfimaopnlem  25600  i1fima  25623  i1fima2  25624  i1fd  25626  c1liplem1  25942  deg1n0ima  26035  efcvx  26399  dvrelog  26586  dvloglem  26597  logf1o2  26599  dvlog  26600  ressatans  26884  wilthlem3  27020  bday1  27794  negsproplem2  28009  negbdaylem  28036  oncutlt  28244  oniso  28251  bdayons  28256  bdayn0p1  28349  trkgbas  28501  trkgdist  28502  trkgitv  28503  ex-ss  30486  ajfval  30869  ipasslem8  30897  hlimcaui  31296  shsspwh  31306  hhssabloi  31322  hhssnv  31324  hhshsslem1  31327  shunssji  31429  sshhococi  31606  pjoml6i  31649  osumcori  31703  mayete3i  31788  mayetes3i  31789  imaelshi  32118  pjclem1  32255  pjci  32260  mdcompli  32489  dmdcompli  32490  xppreima  32707  gsummpt2co  33114  cycpmrn  33209  elrgspnsubrunlem2  33314  evl1deg1  33641  evl1deg2  33642  evl1deg3  33643  circtopn  33987  esumpcvgval  34228  esumcvg  34236  ldgenpisyslem3  34315  elmbfmvol2  34417  sxbrsigalem0  34421  eulerpartlemsv3  34511  ballotlem7  34686  rpsqrtcn  34743  bnj931  34919  bnj1137  35143  fineqvnttrclse  35274  subfacp1lem2a  35368  subfacp1lem2b  35369  erdszelem2  35380  kur14lem7  35400  kur14lem9  35402  dfon2lem2  35970  regsfromunir1  36728  bj-snglsstag  37286  bj-2upln1upl  37329  bj-0int  37411  bj-opabssvv  37462  bj-ccssccbar  37529  bj-ccinftyssccbar  37530  bj-rvecsscvec  37616  icoreelrn  37673  finxpreclem3  37705  imadifss  37907  poimirlem4  37936  poimirlem26  37958  poimirlem27  37959  opnmbllem0  37968  mblfinlem3  37971  mblfinlem4  37972  ismblfin  37973  volsupnfl  37977  sdclem2  38054  heibor1lem  38121  refrelsredund4  39028  dicval  41613  dvhdimlem  41881  ismrc  43132  mapfzcons1cl  43149  2rexfrabdioph  43227  3rexfrabdioph  43228  4rexfrabdioph  43229  6rexfrabdioph  43230  7rexfrabdioph  43231  rabdiophlem2  43233  jm2.27dlem5  43444  algbase  43605  algaddg  43606  algmulr  43607  algsca  43608  algvsca  43609  intimass2  44085  comptiunov2i  44136  relexp0a  44146  lhe4.4ex1a  44759  iocnct  45974  iccnct  45975  dvcosre  46344  fourierdlem46  46584  fourierdlem57  46595  fourierdlem58  46596  fourierdlem62  46600  fourierdlem102  46640  fourierdlem103  46641  fourierdlem104  46642  fourierdlem114  46652  sge0split  46841  sge0uzfsumgt  46876  hoiprodp1  47020  hoidmvlelem1  47027  hoidmvlelem2  47028  hoidmvlelem3  47029  sbgoldbo  48221  usgrexmpl1lem  48455  usgrexmpl2lem  48460  dmmpossx2  48771  ipoglb0  49427  mreclat  49430  catbas  49659  cathomfval  49660  catcofval  49661  aacllem  50234