Theorem sseqtrri 4033

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

Syntax hints:   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3sstr4i  4035  eqimss2i  4045  difsssymdif  4263  snsspr1  4814  snsspr2  4815  snsstp1  4816  snsstp2  4817  snsstp3  4818  unissint  4972  iunxdif2  5053  pwpwssunieq  5104  intabs  5349  inxpssres  5702  elopaelxp  5775  opabssxp  5778  dmresi  6070  cnvimass  6100  sofld  6207  cnvcnv  6212  cnvssrndm  6291  sssucid  6464  f1imadifssran  6652  cnvimainrn  7087  fvclss  7261  dmmpossx  8091  suppun  8209  frrlem12  8322  wfrlem14OLD  8362  tfrlem11  8428  oawordeulem  8592  mapexOLD  8872  trcl  9768  djuunxp  9961  dfac3  10161  cfsuc  10297  isfin4p1  10355  fin23lem11  10357  domtriomlem  10482  ttukeylem1  10549  ttukeylem7  10555  brdom7disj  10571  brdom6disj  10572  fingch  10663  fpwwe2lem12  10682  canthp1lem2  10693  wunex2  10778  wunex3  10781  ressxr  11305  ltrelxr  11322  nnssnn0  12529  un0addcl  12559  un0mulcl  12560  nn0ssxnn0  12602  caubnd  15397  isumclim3  15795  iprodclim3  16036  bpoly4  16095  fprodefsum  16131  znnen  16248  isprm3  16720  phimullem  16816  isstruct2  17186  2strbas  17268  2strop  17269  2strbas1  17272  rngbase  17343  rngplusg  17344  rngmulr  17345  srngbase  17354  srngplusg  17355  srngmulr  17356  srnginvl  17357  lmodbase  17370  lmodplusg  17371  lmodsca  17372  lmodvsca  17373  ipsbase  17381  ipsaddg  17382  ipsmulr  17383  ipssca  17384  ipsvsca  17385  ipsip  17386  phlbase  17391  phlplusg  17392  phlsca  17393  phlvsca  17394  phlip  17395  topgrpbas  17406  topgrpplusg  17407  topgrptset  17408  otpsbas  17421  otpstset  17422  otpsle  17423  odrngbas  17448  odrngplusg  17449  odrngmulr  17450  odrngtset  17451  odrngle  17452  odrngds  17453  homarw  18091  ipoval  18575  ipolerval  18577  eqgfval  19194  cycsubg  19226  symgbas  19389  symgsubmefmndALT  19421  islbs3  21157  cnfldbas  21368  mpocnfldadd  21369  mpocnfldmul  21371  cnfldcj  21373  cnfldtset  21374  cnfldle  21375  cnfldds  21376  cnfldunif  21377  cnfldbasOLD  21383  cnfldaddOLD  21384  cnfldmulOLD  21385  cnfldcjOLD  21386  cnfldtsetOLD  21387  cnfldleOLD  21388  cnflddsOLD  21389  cnfldunifOLD  21390  basdif0  22960  iscldtop  23103  iocpnfordt  23223  icomnfordt  23224  iooordt  23225  cnrest2  23294  cmpcov2  23398  fiuncmp  23412  bwth  23418  indisconn  23426  locfincmp  23534  xkococnlem  23667  hmphdis  23804  uzrest  23905  ufildr  23939  fin1aufil  23940  eltsms  24141  ustval  24211  qtopbaslem  24779  tgqioo  24821  re2ndc  24822  xrhmeo  24977  bndth  24990  pi1xfrcnvlem  25089  ovolficcss  25504  nulmbl2  25571  uniiccdif  25613  opnmbllem  25636  opnmblALT  25638  mbfimaopnlem  25690  i1fima  25713  i1fima2  25714  i1fd  25716  c1liplem1  26035  deg1n0ima  26128  efcvx  26493  dvrelog  26679  dvloglem  26690  logf1o2  26692  dvlog  26693  ressatans  26977  wilthlem3  27113  bday1s  27876  negsproplem2  28061  negsbdaylem  28088  trkgbas  28453  trkgdist  28454  trkgitv  28455  ex-ss  30446  ajfval  30828  ipasslem8  30856  hlimcaui  31255  shsspwh  31265  hhssabloi  31281  hhssnv  31283  hhshsslem1  31286  shunssji  31388  sshhococi  31565  pjoml6i  31608  osumcori  31662  mayete3i  31747  mayetes3i  31748  imaelshi  32077  pjclem1  32214  pjci  32219  mdcompli  32448  dmdcompli  32449  xppreima  32655  gsummpt2co  33051  cycpmrn  33163  elrgspnsubrunlem2  33252  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  circtopn  33836  esumpcvgval  34079  esumcvg  34087  ldgenpisyslem3  34166  elmbfmvol2  34269  sxbrsigalem0  34273  eulerpartlemsv3  34363  ballotlem7  34538  rpsqrtcn  34608  bnj931  34784  bnj1137  35009  subfacp1lem2a  35185  subfacp1lem2b  35186  erdszelem2  35197  kur14lem7  35217  kur14lem9  35219  dfon2lem2  35785  bj-snglsstag  36982  bj-2upln1upl  37025  bj-0int  37102  bj-opabssvv  37151  bj-ccssccbar  37218  bj-ccinftyssccbar  37219  bj-rvecsscvec  37305  icoreelrn  37362  finxpreclem3  37394  imadifss  37602  poimirlem4  37631  poimirlem26  37653  poimirlem27  37654  opnmbllem0  37663  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  volsupnfl  37672  sdclem2  37749  heibor1lem  37816  refrelsredund4  38633  dicval  41178  dvhdimlem  41446  ismrc  42712  mapfzcons1cl  42729  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  rabdiophlem2  42813  jm2.27dlem5  43025  algbase  43186  algaddg  43187  algmulr  43188  algsca  43189  algvsca  43190  intimass2  43668  comptiunov2i  43719  relexp0a  43729  lhe4.4ex1a  44348  iocnct  45553  iccnct  45554  dvcosre  45927  fourierdlem46  46167  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  sge0split  46424  sge0uzfsumgt  46459  hoiprodp1  46603  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  sbgoldbo  47774  usgrexmpl1lem  47980  usgrexmpl2lem  47985  dmmpossx2  48253  ipoglb0  48883  mreclat  48886  aacllem  49320