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  5286  inxpssres  5641  elopaelxp  5714  opabssxp  5716  dmresi  6011  cnvimass  6041  sofld  6145  cnvcnv  6150  cnvssrndm  6229  sssucid  6399  f1imadifssran  6578  cnvimainrn  7013  fvclss  7189  dmmpossx  8012  suppun  8127  frrlem12  8240  tfrlem11  8320  oawordeulem  8482  mapexOLD  8772  trcl  9640  djuunxp  9836  dfac3  10034  cfsuc  10170  isfin4p1  10228  fin23lem11  10230  domtriomlem  10355  ttukeylem1  10422  ttukeylem7  10428  brdom7disj  10444  brdom6disj  10445  fingch  10537  fpwwe2lem12  10556  canthp1lem2  10567  wunex2  10652  wunex3  10655  ressxr  11180  ltrelxr  11197  nnssnn0  12431  un0addcl  12461  un0mulcl  12462  nn0ssxnn0  12504  caubnd  15312  isumclim3  15712  iprodclim3  15956  bpoly4  16015  fprodefsum  16051  znnen  16170  isprm3  16643  phimullem  16740  isstruct2  17110  2strbas  17189  rngbase  17253  rngplusg  17254  rngmulr  17255  srngbase  17264  srngplusg  17265  srngmulr  17266  srnginvl  17267  lmodbase  17280  lmodplusg  17281  lmodsca  17282  lmodvsca  17283  ipsbase  17291  ipsaddg  17292  ipsmulr  17293  ipssca  17294  ipsvsca  17295  ipsip  17296  phlbase  17301  phlplusg  17302  phlsca  17303  phlvsca  17304  phlip  17305  topgrpbas  17316  topgrpplusg  17317  topgrptset  17318  otpsbas  17331  otpstset  17332  otpsle  17333  odrngbas  17358  odrngplusg  17359  odrngmulr  17360  odrngtset  17361  odrngle  17362  odrngds  17363  homarw  18004  ipoval  18487  ipolerval  18489  eqgfval  19142  cycsubg  19174  symgbas  19338  symgsubmefmndALT  19369  islbs3  21145  cnfldbas  21348  mpocnfldadd  21349  mpocnfldmul  21351  cnfldcj  21353  cnfldtset  21354  cnfldle  21355  cnfldds  21356  cnfldunif  21357  cnfldbasOLD  21363  cnfldaddOLD  21364  cnfldmulOLD  21365  cnfldcjOLD  21366  cnfldtsetOLD  21367  cnfldleOLD  21368  cnflddsOLD  21369  cnfldunifOLD  21370  basdif0  22928  iscldtop  23070  iocpnfordt  23190  icomnfordt  23191  iooordt  23192  cnrest2  23261  cmpcov2  23365  fiuncmp  23379  bwth  23385  indisconn  23393  locfincmp  23501  xkococnlem  23634  hmphdis  23771  uzrest  23872  ufildr  23906  fin1aufil  23907  eltsms  24108  ustval  24178  qtopbaslem  24733  tgqioo  24775  re2ndc  24776  xrhmeo  24923  bndth  24935  pi1xfrcnvlem  25033  ovolficcss  25446  nulmbl2  25513  uniiccdif  25555  opnmbllem  25578  opnmblALT  25580  mbfimaopnlem  25632  i1fima  25655  i1fima2  25656  i1fd  25658  c1liplem1  25973  deg1n0ima  26064  efcvx  26427  dvrelog  26614  dvloglem  26625  logf1o2  26627  dvlog  26628  ressatans  26911  wilthlem3  27047  bday1  27820  negsproplem2  28035  negbdaylem  28062  oncutlt  28270  oniso  28277  bdayons  28282  bdayn0p1  28375  trkgbas  28527  trkgdist  28528  trkgitv  28529  ex-ss  30512  ajfval  30895  ipasslem8  30923  hlimcaui  31322  shsspwh  31332  hhssabloi  31348  hhssnv  31350  hhshsslem1  31353  shunssji  31455  sshhococi  31632  pjoml6i  31675  osumcori  31729  mayete3i  31814  mayetes3i  31815  imaelshi  32144  pjclem1  32281  pjci  32286  mdcompli  32515  dmdcompli  32516  xppreima  32733  gsummpt2co  33124  cycpmrn  33219  elrgspnsubrunlem2  33324  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  circtopn  33997  esumpcvgval  34238  esumcvg  34246  ldgenpisyslem3  34325  elmbfmvol2  34427  sxbrsigalem0  34431  eulerpartlemsv3  34521  ballotlem7  34696  rpsqrtcn  34753  bnj931  34929  bnj1137  35153  fineqvnttrclse  35284  subfacp1lem2a  35378  subfacp1lem2b  35379  erdszelem2  35390  kur14lem7  35410  kur14lem9  35412  dfon2lem2  35980  regsfromunir1  36738  bj-snglsstag  37304  bj-2upln1upl  37347  bj-0int  37429  bj-opabssvv  37480  bj-ccssccbar  37547  bj-ccinftyssccbar  37548  bj-rvecsscvec  37634  icoreelrn  37691  finxpreclem3  37723  imadifss  37930  poimirlem4  37959  poimirlem26  37981  poimirlem27  37982  opnmbllem0  37991  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  volsupnfl  38000  sdclem2  38077  heibor1lem  38144  refrelsredund4  39051  dicval  41636  dvhdimlem  41904  ismrc  43147  mapfzcons1cl  43164  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  rabdiophlem2  43248  jm2.27dlem5  43459  algbase  43620  algaddg  43621  algmulr  43622  algsca  43623  algvsca  43624  intimass2  44100  comptiunov2i  44151  relexp0a  44161  lhe4.4ex1a  44774  iocnct  45988  iccnct  45989  dvcosre  46358  fourierdlem46  46598  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  sge0split  46855  sge0uzfsumgt  46890  hoiprodp1  47034  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  sbgoldbo  48275  usgrexmpl1lem  48509  usgrexmpl2lem  48514  dmmpossx2  48825  ipoglb0  49481  mreclat  49484  catbas  49713  cathomfval  49714  catcofval  49715  aacllem  50288