Theorem sseqtrri 3980

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

Syntax hints:   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  3sstr4i  3982  eqimss2i  3992  difsssymdif  4212  snsspr1  4765  snsspr2  4766  snsstp1  4767  snsstp2  4768  snsstp3  4769  unissint  4922  iunxdif2  5004  pwpwssunieq  5054  intabs  5289  inxpssres  5636  elopaelxp  5709  opabssxp  5711  dmresi  6005  cnvimass  6035  sofld  6139  cnvcnv  6144  cnvssrndm  6223  sssucid  6393  f1imadifssran  6572  cnvimainrn  7006  fvclss  7181  dmmpossx  8004  suppun  8120  frrlem12  8233  tfrlem11  8313  oawordeulem  8475  mapexOLD  8762  trcl  9625  djuunxp  9821  dfac3  10019  cfsuc  10155  isfin4p1  10213  fin23lem11  10215  domtriomlem  10340  ttukeylem1  10407  ttukeylem7  10413  brdom7disj  10429  brdom6disj  10430  fingch  10521  fpwwe2lem12  10540  canthp1lem2  10551  wunex2  10636  wunex3  10639  ressxr  11163  ltrelxr  11180  nnssnn0  12391  un0addcl  12421  un0mulcl  12422  nn0ssxnn0  12464  caubnd  15268  isumclim3  15668  iprodclim3  15909  bpoly4  15968  fprodefsum  16004  znnen  16123  isprm3  16596  phimullem  16692  isstruct2  17062  2strbas  17141  rngbase  17205  rngplusg  17206  rngmulr  17207  srngbase  17216  srngplusg  17217  srngmulr  17218  srnginvl  17219  lmodbase  17232  lmodplusg  17233  lmodsca  17234  lmodvsca  17235  ipsbase  17243  ipsaddg  17244  ipsmulr  17245  ipssca  17246  ipsvsca  17247  ipsip  17248  phlbase  17253  phlplusg  17254  phlsca  17255  phlvsca  17256  phlip  17257  topgrpbas  17268  topgrpplusg  17269  topgrptset  17270  otpsbas  17283  otpstset  17284  otpsle  17285  odrngbas  17310  odrngplusg  17311  odrngmulr  17312  odrngtset  17313  odrngle  17314  odrngds  17315  homarw  17955  ipoval  18438  ipolerval  18440  eqgfval  19090  cycsubg  19122  symgbas  19286  symgsubmefmndALT  19317  islbs3  21094  cnfldbas  21297  mpocnfldadd  21298  mpocnfldmul  21300  cnfldcj  21302  cnfldtset  21303  cnfldle  21304  cnfldds  21305  cnfldunif  21306  cnfldbasOLD  21312  cnfldaddOLD  21313  cnfldmulOLD  21314  cnfldcjOLD  21315  cnfldtsetOLD  21316  cnfldleOLD  21317  cnflddsOLD  21318  cnfldunifOLD  21319  basdif0  22869  iscldtop  23011  iocpnfordt  23131  icomnfordt  23132  iooordt  23133  cnrest2  23202  cmpcov2  23306  fiuncmp  23320  bwth  23326  indisconn  23334  locfincmp  23442  xkococnlem  23575  hmphdis  23712  uzrest  23813  ufildr  23847  fin1aufil  23848  eltsms  24049  ustval  24119  qtopbaslem  24674  tgqioo  24716  re2ndc  24717  xrhmeo  24872  bndth  24885  pi1xfrcnvlem  24984  ovolficcss  25398  nulmbl2  25465  uniiccdif  25507  opnmbllem  25530  opnmblALT  25532  mbfimaopnlem  25584  i1fima  25607  i1fima2  25608  i1fd  25610  c1liplem1  25929  deg1n0ima  26022  efcvx  26387  dvrelog  26574  dvloglem  26585  logf1o2  26587  dvlog  26588  ressatans  26872  wilthlem3  27008  bday1s  27776  negsproplem2  27972  negsbdaylem  27999  onscutlt  28202  onsiso  28206  bdayon  28210  bdayn0p1  28295  trkgbas  28424  trkgdist  28425  trkgitv  28426  ex-ss  30409  ajfval  30791  ipasslem8  30819  hlimcaui  31218  shsspwh  31228  hhssabloi  31244  hhssnv  31246  hhshsslem1  31249  shunssji  31351  sshhococi  31528  pjoml6i  31571  osumcori  31625  mayete3i  31710  mayetes3i  31711  imaelshi  32040  pjclem1  32177  pjci  32182  mdcompli  32411  dmdcompli  32412  xppreima  32629  gsummpt2co  33035  cycpmrn  33119  elrgspnsubrunlem2  33222  evl1deg1  33546  evl1deg2  33547  evl1deg3  33548  circtopn  33871  esumpcvgval  34112  esumcvg  34120  ldgenpisyslem3  34199  elmbfmvol2  34301  sxbrsigalem0  34305  eulerpartlemsv3  34395  ballotlem7  34570  rpsqrtcn  34627  bnj931  34803  bnj1137  35028  fineqvnttrclse  35165  subfacp1lem2a  35245  subfacp1lem2b  35246  erdszelem2  35257  kur14lem7  35277  kur14lem9  35279  dfon2lem2  35847  bj-snglsstag  37046  bj-2upln1upl  37089  bj-0int  37166  bj-opabssvv  37215  bj-ccssccbar  37282  bj-ccinftyssccbar  37283  bj-rvecsscvec  37369  icoreelrn  37426  finxpreclem3  37458  imadifss  37655  poimirlem4  37684  poimirlem26  37706  poimirlem27  37707  opnmbllem0  37716  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  volsupnfl  37725  sdclem2  37802  heibor1lem  37869  refrelsredund4  38748  dicval  41295  dvhdimlem  41563  ismrc  42818  mapfzcons1cl  42835  2rexfrabdioph  42913  3rexfrabdioph  42914  4rexfrabdioph  42915  6rexfrabdioph  42916  7rexfrabdioph  42917  rabdiophlem2  42919  jm2.27dlem5  43130  algbase  43291  algaddg  43292  algmulr  43293  algsca  43294  algvsca  43295  intimass2  43772  comptiunov2i  43823  relexp0a  43833  lhe4.4ex1a  44446  iocnct  45664  iccnct  45665  dvcosre  46034  fourierdlem46  46274  fourierdlem57  46285  fourierdlem58  46286  fourierdlem62  46290  fourierdlem102  46330  fourierdlem103  46331  fourierdlem104  46332  fourierdlem114  46342  sge0split  46531  sge0uzfsumgt  46566  hoiprodp1  46710  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  sbgoldbo  47911  usgrexmpl1lem  48145  usgrexmpl2lem  48150  dmmpossx2  48461  ipoglb0  49118  mreclat  49121  catbas  49351  cathomfval  49352  catcofval  49353  aacllem  49926