Theorem sseqtrri 3983

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  3sstr4i  3985  eqimss2i  3995  difsssymdif  4212  snsspr1  4778  snsspr2  4779  snsstp1  4780  snsstp2  4781  snsstp3  4782  unissint  4935  iunxdif2  5016  pwpwssunieq  5068  intabs  5317  inxpssres  5676  elopaelxp  5749  opabssxp  5751  dmresi  6052  cnvimass  6082  sofld  6184  cnvcnv  6189  imadifssran  6201  cnvssrndm  6272  sssucid  6444  cnvimainrn  7063  fvclss  7242  dmmpossx  8067  suppun  8186  frrlem12  8300  tfrlem11  8381  oawordeulem  8545  trcl  9711  djuunxp  9930  dfac3  10128  cfsuc  10263  isfin4p1  10321  fin23lem11  10323  domtriomlem  10448  ttukeylem1  10515  ttukeylem7  10521  brdom7disj  10538  brdom6disj  10539  fingch  10636  fpwwe2lem12  10655  canthp1lem2  10666  wunex2  10751  wunex3  10754  ressxr  11281  ltrelxr  11298  nnssnn0  12535  un0addcl  12565  un0mulcl  12566  nn0ssxnn0  12608  caubnd  15450  isumclim3  15849  iprodclim3  16093  bpoly4  16151  fprodefsum  16187  znnen  16306  isprm3  16779  phimullem  16876  isstruct2  17247  2strbas  17326  rngbase  17390  rngplusg  17391  rngmulr  17392  srngbase  17401  srngplusg  17402  srngmulr  17403  srnginvl  17404  lmodbase  17417  lmodplusg  17418  lmodsca  17419  lmodvsca  17420  ipsbase  17428  ipsaddg  17429  ipsmulr  17430  ipssca  17431  ipsvsca  17432  ipsip  17433  phlbase  17438  phlplusg  17439  phlsca  17440  phlvsca  17441  phlip  17442  topgrpbas  17453  topgrpplusg  17454  topgrptset  17455  otpsbas  17468  otpstset  17469  otpsle  17470  odrngbas  17495  odrngplusg  17496  odrngmulr  17497  odrngtset  17498  odrngle  17499  odrngds  17500  homarw  18141  ipoval  18624  ipolerval  18626  eqgfval  19307  cycsubg  19342  symgbas  19505  symgsubmefmndALT  19536  islbs3  21348  cnfldbas  21595  mpocnfldadd  21596  mpocnfldmul  21598  cnfldcj  21600  cnfldtset  21601  cnfldle  21602  cnfldds  21603  cnfldunif  21604  basdif0  23184  iscldtop  23326  iocpnfordt  23446  icomnfordt  23447  iooordt  23448  cnrest2  23517  cmpcov2  23621  fiuncmp  23635  bwth  23641  indisconn  23649  locfincmp  23758  xkococnlem  23891  hmphdis  24028  uzrest  24129  ufildr  24163  fin1aufil  24164  eltsms  24365  ustval  24435  qtopbaslem  24990  tgqioo  25032  re2ndc  25033  xrhmeo  25180  bndth  25192  pi1xfrcnvlem  25290  ovolficcss  25703  nulmbl2  25770  uniiccdif  25812  opnmbllem  25835  opnmblALT  25837  mbfimaopnlem  25889  i1fima  25912  i1fima2  25913  i1fd  25915  c1liplem1  26230  deg1n0ima  26321  efcvx  26692  dvrelog  26882  dvloglem  26893  logf1o2  26895  dvlog  26896  ressatans  27179  wilthlem3  27314  bday1  28087  negsproplem2  28302  negbdaylem  28329  oncutlt  28537  oniso  28544  bdayons  28549  bdayn0p1  28642  trkgbas  28794  trkgdist  28795  trkgitv  28796  ex-ss  30915  ajfval  31298  ipasslem8  31326  hlimcaui  31725  shsspwh  31735  hhssabloi  31751  hhssnv  31753  hhshsslem1  31756  shunssji  31858  sshhococi  32035  pjoml6i  32078  osumcori  32132  mayete3i  32217  mayetes3i  32218  imaelshi  32547  pjclem1  32684  pjci  32689  mdcompli  32918  dmdcompli  32919  xppreima  33126  gsummpt2co  33496  cycpmrn  33591  elrgspnsubrunlem2  33696  evl1deg1  33994  evl1deg2  33995  evl1deg3  33996  circtopn  34355  esumpcvgval  34596  esumcvg  34604  ldgenpisyslem3  34684  elmbfmvol2  34786  sxbrsigalem0  34790  eulerpartlemsv3  34880  ballotlem7  35055  rpsqrtcn  35109  bnj931  35288  bnj1137  35512  fineqvnttrclse  35658  subfacp1lem2a  35767  subfacp1lem2b  35768  erdszelem2  35779  kur14lem7  35799  kur14lem9  35801  dfon2lem2  36369  regsfromunir1  37167  bj-snglsstag  37733  bj-2upln1upl  37776  bj-0int  37859  bj-opabssvv  37910  bj-ccssccbar  37977  bj-ccinftyssccbar  37978  bj-rvecsscvec  38064  icoreelrn  38123  finxpreclem3  38155  imadifss  38362  poimirlem4  38381  poimirlem26  38403  poimirlem27  38404  opnmbllem0  38413  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  volsupnfl  38422  sdclem2  38500  heibor1lem  38567  refrelsredund4  39472  dicval  42057  dvhdimlem  42325  ismrc  43554  mapfzcons1cl  43571  2rexfrabdioph  43645  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  rabdiophlem2  43651  jm2.27dlem5  43862  algbase  44023  algaddg  44024  algmulr  44025  algsca  44026  algvsca  44027  intimass2  44503  comptiunov2i  44554  relexp0a  44564  lhe4.4ex1a  45161  iocnct  46378  iccnct  46379  dvcosre  46748  fourierdlem46  46988  fourierdlem57  46999  fourierdlem58  47000  fourierdlem62  47004  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem114  47056  sge0split  47245  sge0uzfsumgt  47280  hoiprodp1  47424  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  sbgoldbo  48711  usgrexmpl1lem  48945  usgrexmpl2lem  48950  dmmpossx2  49275  ipoglb0  49928  mreclat  49931  catbas  50160  cathomfval  50161  catcofval  50162  aacllem  50780