Theorem eqsstri 4016

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)

Hypotheses

Ref	Expression
eqsstr.1	⊢ 𝐴 = 𝐵
eqsstr.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 ⊢ 𝐵 ⊆ 𝐶
2		eqsstr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 4010	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 230	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  eqsstrri  4017  ssrab2OLD  4078  ssrab3  4080  rabssab  4083  ifssun  4545  opabss  5212  brab2a  5769  relopabiALT  5823  dmopabss  5918  resss  6006  relres  6010  rnin  6146  rnxpss  6171  cnvcnvss  6193  resdmss  6234  resssxp  6269  dfpo2  6295  predss  6308  fnres  6677  f0  6772  nfvres  6932  fvopab4ndm  7027  ffvresb  7126  mptexgf  7226  funiunfv  7249  isoini2  7338  ovssunirn  7447  dmoprabss  7513  mpondm0  7649  elmpocl  7650  exse2  7910  fabexg  7927  frxp  8114  tposssxp  8217  dftpos4  8232  wfrdmssOLD  8317  smores  8354  smores2  8356  iordsmo  8359  swoer  8735  swoord1  8736  swoord2  8737  ecss  8751  ecopovsym  8815  ecopovtrn  8816  ecopover  8817  f1setex  8853  sbthlem7  9091  nnfiOLD  9234  imafiALT  9347  elfiun  9427  marypha1lem  9430  marypha2lem1  9432  hartogslem1  9539  wdomima2g  9583  inf3lem1  9625  dmttrcl  9718  rnttrcl  9719  tc2  9739  frmin  9746  frrlem16  9755  frr1  9756  tz9.12lem1  9784  rankuni  9860  rankuniss  9863  rankmapu  9875  hta  9894  r0weon  10009  infxpenlem  10010  ackbij1lem9  10225  ackbij1lem10  10226  ackbij1b  10236  sdom2en01  10299  fin23lem26  10322  fin56  10390  fin1a2lem9  10405  axdc3lem  10447  axdc3lem2  10448  axcclem  10454  imadomg  10531  iundom2g  10537  smobeth  10583  canth4  10644  gruina  10815  grur1a  10816  pinn  10875  niex  10878  ltsopi  10885  ltrelpi  10886  dmaddpi  10887  dmmulpi  10888  enqex  10919  ltrelnq  10923  nqerf  10927  nqerrel  10929  dmrecnq  10965  lterpq  10967  ltrelpr  10995  enrex  11064  ltrelsr  11065  dmaddsr  11082  dmmulsr  11083  ltrelre  11131  axaddf  11142  axmulf  11143  ltrelxr  11279  lerelxr  11281  nn0ssre  12480  nn0sscn  12481  nn0ssz  12585  uzsupss  12928  rpnnen1lem1  12966  rpnnen1lem3  12967  rpnnen1lem5  12969  fz1ssfz0  13601  uzsup  13832  fzfi  13941  swrd00  14598  01sqrexlem3  15195  cau3  15306  caubnd  15309  limsupgre  15429  rlimpm  15448  rlimclim  15494  isercolllem1  15615  isercolllem2  15616  isercoll  15618  caurcvg  15627  caucvg  15629  iseraltlem2  15633  iseraltlem3  15634  zsum  15668  fsumcvg3  15679  climfsum  15770  ackbijnn  15778  divcnvshft  15805  infcvgaux1i  15807  clim2prod  15838  ntrivcvg  15847  ntrivcvgfvn0  15849  ntrivcvgtail  15850  ntrivcvgmullem  15851  ntrivcvgmul  15852  zprod  15885  dvdszrcl  16206  4sqlem1  16885  4sqlem19  16900  ramub1lem2  16964  structcnvcnv  17090  strleun  17094  fvsetsid  17105  smndex1sgrp  18825  gicer  19191  cntzsgrpcl  19239  symgbasfi  19287  mvdco  19354  symgsssg  19376  efglem  19625  efgtf  19631  efgtlen  19635  efginvrel2  19636  efginvrel1  19637  efgsfo  19648  efgredlemg  19651  efgredleme  19652  efgredlemd  19653  efgredlemc  19654  efgredlem  19656  efgred  19657  efgrelexlemb  19659  efgcpbllemb  19664  frgpinv  19673  frgpuplem  19681  frgpupf  19682  frgpup1  19684  frgpnabllem2  19783  gsumval3lem1  19814  gsumval3lem2  19815  gsumval3  19816  lbsextlem3  20918  pzriprnglem10  21259  znf1o  21326  zntoslem  21331  pjpm  21482  mhp0cl  21908  ply1bascl  21946  dmtopon  22645  ordtbas  22916  leordtval2  22936  lecldbas  22943  lmfval  22956  lmbrf  22984  cnconst2  23007  conncompcld  23158  hauspwdom  23225  txuni2  23289  xkouni  23323  xkoccn  23343  txkgen  23376  qtoptop2  23423  kqdisj  23456  hmphtop  23502  hmpher  23508  uzrest  23621  uzfbas  23622  lmflf  23729  tgpconncompeqg  23836  tgpconncomp  23837  ustn0  23945  xmeter  24159  isngp2  24326  xrtgioo  24542  iccntr  24557  xmetdcn  24574  metdcn  24576  metdscn2  24593  icchmeo  24681  cnheiborlem  24694  lmmbrf  25003  iscau4  25020  iscauf  25021  caucfil  25024  lmclimf  25045  volf  25270  uniioombllem3  25326  uniioombllem4  25327  uniioombllem5  25328  volcn  25347  mbfimaopnlem  25396  mbflimsup  25407  i1f1  25431  itg2lcl  25469  itgioo  25557  itgsplitioo  25579  limcflflem  25621  limcflf  25622  limcresi  25626  lhop  25757  dvfsumlem1  25767  dvfsumlem2  25768  dvfsumlem3  25769  dvfsumlem4  25770  dvfsumrlimge0  25771  dvfsumrlim  25772  dvfsumrlim2  25773  dvfsum2  25775  vieta1lem1  26047  vieta1lem2  26048  psercnlem2  26160  psercnlem1  26161  psercn  26162  pserdvlem1  26163  pserdvlem2  26164  pserdv  26165  pserdv2  26166  logcnlem5  26378  dvlog  26383  dvlog2lem  26384  dvlog2  26385  dvcncxp1  26475  dvcnsqrt  26476  cxpcn3lem  26479  cxpcn3  26480  sqrtcn  26482  1cubr  26571  atansssdm  26662  jensen  26717  musum  26919  ppiub  26931  lgsquadlem1  27107  lgsquadlem2  27108  lgsquadlem3  27109  2sqlem7  27151  nosupbnd1lem1  27435  nosupbnd2  27443  noinfbnd1lem1  27450  scutf  27538  leftssold  27598  rightssold  27599  mulsproplem12  27810  mulsproplem13  27811  mulsproplem14  27812  precsexlem8  27887  onssno  27908  nnssn0s  27925  axtgcgrrflx  27968  axtgcgrid  27969  axtgsegcon  27970  axtg5seg  27971  axtgbtwnid  27972  axtgpasch  27973  axtgcont1  27974  tglng  28052  disjxwwlkn  29422  frgrwopreg2  29827  phnv  30322  htthlem  30425  hlimadd  30701  hlimcaui  30744  hhsscms  30786  occllem  30811  shjshsi  31000  3oalem4  31173  pjfi  31212  dmadjss  31395  nlelshi  31568  nlelchi  31569  hmopidmchi  31659  shatomistici  31869  difxp1ss  32015  difxp2ss  32016  fcoinver  32090  opabssi  32097  mptctf  32197  gsumpart  32465  pmtrcnel2  32509  psgnfzto1stlem  32517  cycpmrn  32560  cyc3genpm  32569  lsmsnorb  32763  ply1degltel  32928  ply1degleel  32929  ply1degltlss  32930  cnre2csqima  33177  raddcn  33195  rrhre  33287  esumsnf  33348  sxbrsiga  33575  omssubadd  33585  carsggect  33603  sitmcl  33636  oddpwdc  33639  eulerpartlem1  33652  eulerpartlemt  33656  eulerpartgbij  33657  eulerpartlemmf  33660  eulerpartlemgh  33663  sseqf  33677  ballotlemfmpn  33779  ballotth  33822  signswch  33858  ftc2re  33896  fdvposlt  33897  fdvposle  33899  bnj1146  34088  bnj1292  34112  bnj1293  34113  bnj1145  34290  bnj1177  34303  erdszelem2  34469  kur14lem3  34485  kur14lem6  34488  kur14lem7  34489  kur14lem9  34491  cvmlift2lem12  34591  mpstssv  34816  mstapst  34824  mppspstlem  34848  mppspst  34851  mthmsta  34855  mthmpps  34859  mclsppslem  34860  txpss3v  35142  pprodss4v  35148  relsset  35152  fixssdm  35170  fixssrn  35171  limitssson  35175  funpartss  35208  colinearex  35324  gg-reparphti  35458  gg-dvfsumlem2  35469  fneer  35541  neibastop1  35547  neibastop2lem  35548  filnetlem2  35567  filnetlem3  35568  knoppcnlem10  35681  bj-tagss  36164  bj-imdirco  36374  bj-fvsnun2  36440  bj-ablssgrp  36460  bj-ablsscmn  36462  bj-vecssmod  36465  bj-fldssdrng  36472  icoreresf  36536  icoreunrn  36543  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimir  36824  broucube  36825  dvasin  36875  dvacos  36876  areacirc  36884  caures  36931  bnd2lem  36962  ismtyres  36979  flddivrng  37170  xrnss3v  37545  refrelsredund2  37806  toycom  38146  dihglblem2N  40468  lcdvbase  40767  mapdunirnN  40824  prjspreln0  41653  prjspvs  41654  prjspeclsp  41656  0prjspnrel  41671  dffltz  41678  eldiophb  41797  monotuz  41982  pwssplit4  42133  pwfi2f1o  42140  arearect  42266  cantnfresb  42376  omabs2  42384  fvnonrel  42650  rclexi  42668  rtrclex  42670  trclexi  42673  rtrclexi  42674  clcnvlem  42676  cnvrcl0  42678  cnvtrcl0  42679  dfrtrcl5  42682  dfrcl2  42727  comptiunov2i  42759  corclrcl  42760  trclrelexplem  42764  relexpaddss  42771  cotrcltrcl  42778  corcltrcl  42792  cotrclrcl  42795  frege131d  42817  0he  42835  grumnudlem  43346  uzmptshftfval  43407  binomcxplemdvbinom  43414  binomcxplemdvsum  43416  binomcxplemnotnn0  43417  rabexgf  44010  uzct  44052  disjf1o  44189  dmresss  44232  dmmptssf  44233  mptssid  44243  uzfissfz  44335  ssuzfz  44358  uzssre2  44416  uzublem  44439  uzssz2  44465  uzsscn2  44487  sumnnodd  44645  climconstmpt  44673  fnlimfvre  44689  fnlimabslt  44694  limsupvaluz  44723  limsupubuzlem  44727  limsupubuz  44728  limsupequzmpt2  44733  limsupmnfuzlem  44741  limsupre3uzlem  44750  liminfequzmpt2  44806  ibliooicc  44986  stoweidlem44  45059  stoweidlem50  45065  stoweidlem51  45066  stoweidlem52  45067  stoweidlem57  45072  stoweidlem59  45074  fourierdlem16  45138  fourierdlem19  45141  fourierdlem21  45143  fourierdlem22  45144  fourierdlem42  45164  fourierdlem83  45204  fouriersw  45246  salexct  45349  salexct3  45357  salgencntex  45358  salgensscntex  45359  sge0less  45407  sge0fodjrnlem  45431  sge0isum  45442  ovnlerp  45577  ovn0lem  45580  hoidmv1lelem1  45606  hoidmv1lelem3  45608  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  ovnhoilem1  45616  ovnhoilem2  45617  opnvonmbllem2  45648  ovolval4lem1  45664  ovolval5lem3  45669  pimdecfgtioc  45730  pimincfltioc  45731  pimdecfgtioo  45732  pimincfltioo  45733  incsmflem  45756  decsmflem  45781  smflimlem2  45787  smflimlem3  45788  smflim  45792  smfrec  45804  smfmullem4  45809  smfdiv  45812  smfsuplem1  45826  smfsuplem3  45828  smfsupxr  45831  smfliminflem  45845  cfsetssfset  46065  fcoreslem2  46073  fcores  46076  oddibas  46850  2zlidl  46921  2zrngbas  46923  2zrng0  46925  fldc  47070  fldhmsubc  47071  fldcALTV  47088  fldhmsubcALTV  47089  ipolub0  47705