Theorem sseqtrri 3963

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

Syntax hints:   = wceq 1539   ⊆ wss 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  eqimss2i  3985  difsssymdif  4192  snsspr1  4753  snsspr2  4754  snsstp1  4755  snsstp2  4756  snsstp3  4757  unissint  4910  iunxdif2  4990  pwpwssunieq  5040  intabs  5275  inxpssres  5617  elopaelxp  5687  opabssxp  5690  dmresi  5971  cnvimass  5999  sofld  6105  cnvcnv  6110  cnvssrndm  6189  sssucid  6360  cnvimainrn  6976  fvclss  7147  dmmpossx  7938  suppun  8031  frrlem12  8144  wfrlem14OLD  8184  tfrlem11  8250  oawordeulem  8416  mapex  8652  trcl  9530  djuunxp  9723  dfac3  9923  cfsuc  10059  isfin4p1  10117  fin23lem11  10119  domtriomlem  10244  ttukeylem1  10311  ttukeylem7  10317  brdom7disj  10333  brdom6disj  10334  fingch  10425  fpwwe2lem12  10444  canthp1lem2  10455  wunex2  10540  wunex3  10543  ressxr  11065  ltrelxr  11082  nnssnn0  12282  un0addcl  12312  un0mulcl  12313  nn0ssxnn0  12354  caubnd  15115  isumclim3  15516  iprodclim3  15755  bpoly4  15814  fprodefsum  15849  znnen  15966  isprm3  16433  phimullem  16525  isstruct2  16895  2strbas  16980  2strop  16981  2strbas1  16984  rngbase  17054  rngplusg  17055  rngmulr  17056  srngbase  17065  srngplusg  17066  srngmulr  17067  srnginvl  17068  lmodbase  17081  lmodplusg  17082  lmodsca  17083  lmodvsca  17084  ipsbase  17092  ipsaddg  17093  ipsmulr  17094  ipssca  17095  ipsvsca  17096  ipsip  17097  phlbase  17102  phlplusg  17103  phlsca  17104  phlvsca  17105  phlip  17106  topgrpbas  17117  topgrpplusg  17118  topgrptset  17119  otpsbas  17132  otpstset  17133  otpsle  17134  odrngbas  17159  odrngplusg  17160  odrngmulr  17161  odrngtset  17162  odrngle  17163  odrngds  17164  homarw  17806  ipoval  18293  ipolerval  18295  eqgfval  18849  cycsubg  18872  symgbas  19023  symgsubmefmndALT  19056  islbs3  20462  cnfldbas  20646  cnfldadd  20647  cnfldmul  20648  cnfldcj  20649  cnfldtset  20650  cnfldle  20651  cnfldds  20652  cnfldunif  20653  basdif0  22148  iscldtop  22291  iocpnfordt  22411  icomnfordt  22412  iooordt  22413  cnrest2  22482  cmpcov2  22586  fiuncmp  22600  bwth  22606  indisconn  22614  locfincmp  22722  xkococnlem  22855  hmphdis  22992  uzrest  23093  ufildr  23127  fin1aufil  23128  eltsms  23329  ustval  23399  qtopbaslem  23967  tgqioo  24008  re2ndc  24009  xrhmeo  24154  bndth  24166  pi1xfrcnvlem  24264  ovolficcss  24678  nulmbl2  24745  uniiccdif  24787  opnmbllem  24810  opnmblALT  24812  mbfimaopnlem  24864  i1fima  24887  i1fima2  24888  i1fd  24890  c1liplem1  25205  deg1n0ima  25299  efcvx  25653  dvrelog  25837  dvloglem  25848  logf1o2  25850  dvlog  25851  ressatans  26129  wilthlem3  26264  trkgbas  26851  trkgdist  26852  trkgitv  26853  ex-ss  28836  ajfval  29216  ipasslem8  29244  hlimcaui  29643  shsspwh  29653  hhssabloi  29669  hhssnv  29671  hhshsslem1  29674  shunssji  29776  sshhococi  29953  pjoml6i  29996  osumcori  30050  mayete3i  30135  mayetes3i  30136  imaelshi  30465  pjclem1  30602  pjci  30607  mdcompli  30836  dmdcompli  30837  xppreima  31028  gsummpt2co  31353  cycpmrn  31455  circtopn  31832  esumpcvgval  32091  esumcvg  32099  ldgenpisyslem3  32178  elmbfmvol2  32279  sxbrsigalem0  32283  eulerpartlemsv3  32373  ballotlem7  32547  rpsqrtcn  32618  bnj931  32795  bnj1137  33020  subfacp1lem2a  33187  subfacp1lem2b  33188  erdszelem2  33199  kur14lem7  33219  kur14lem9  33221  dfon2lem2  33805  bday1s  34070  bj-snglsstag  35215  bj-2upln1upl  35258  bj-0int  35316  bj-opabssvv  35365  bj-ccssccbar  35432  bj-ccinftyssccbar  35433  bj-rvecsscvec  35519  icoreelrn  35576  finxpreclem3  35608  imadifss  35796  poimirlem4  35825  poimirlem26  35847  poimirlem27  35848  opnmbllem0  35857  mblfinlem3  35860  mblfinlem4  35861  ismblfin  35862  volsupnfl  35866  sdclem2  35944  heibor1lem  36011  refrelsredund4  36787  dicval  39232  dvhdimlem  39500  ismrc  40560  mapfzcons1cl  40577  2rexfrabdioph  40655  3rexfrabdioph  40656  4rexfrabdioph  40657  6rexfrabdioph  40658  7rexfrabdioph  40659  rabdiophlem2  40661  jm2.27dlem5  40873  algbase  41041  algaddg  41042  algmulr  41043  algsca  41044  algvsca  41045  intimass2  41301  comptiunov2i  41352  relexp0a  41362  lhe4.4ex1a  41985  iocnct  43127  iccnct  43128  dvcosre  43502  fourierdlem46  43742  fourierdlem57  43753  fourierdlem58  43754  fourierdlem62  43758  fourierdlem102  43798  fourierdlem103  43799  fourierdlem104  43800  fourierdlem114  43810  sge0split  43997  sge0uzfsumgt  44032  hoiprodp1  44176  hoidmvlelem1  44183  hoidmvlelem2  44184  hoidmvlelem3  44185  sbgoldbo  45297  dmmpossx2  45730  ipoglb0  46338  mreclat  46341  aacllem  46563