Theorem eqsstri 4001

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 3995	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 233	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1537   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqsstrri  4002  ssrab2  4056  ssrab3  4057  rabssab  4060  opabss  5130  brab2a  5644  relopabiALT  5695  dmopabss  5787  resss  5878  relres  5882  rnin  6005  rnxpss  6029  cnvcnvss  6051  predss  6155  fnres  6474  f0  6560  nfvres  6706  fvopab4ndm  6797  ffvresb  6888  mptexgf  6985  funiunfv  7007  isoini2  7092  ovssunirn  7192  dmoprabss  7256  mpondm0  7386  elmpocl  7387  exse2  7622  fabexg  7639  frxp  7820  tposssxp  7896  dftpos4  7911  wfrdmss  7961  smores  7989  smores2  7991  iordsmo  7994  swoer  8319  swoord1  8320  swoord2  8321  ecss  8335  ecopovsym  8399  ecopovtrn  8400  ecopover  8401  sbthlem7  8633  nnfi  8711  imafi  8817  elfiun  8894  marypha1lem  8897  marypha2lem1  8899  hartogslem1  9006  wdomima2g  9050  inf3lem1  9091  tc2  9184  tz9.12lem1  9216  rankuni  9292  rankuniss  9295  rankmapu  9307  hta  9326  r0weon  9438  infxpenlem  9439  ackbij1lem9  9650  ackbij1lem10  9651  ackbij1b  9661  sdom2en01  9724  fin23lem26  9747  fin56  9815  fin1a2lem9  9830  axdc3lem  9872  axdc3lem2  9873  axcclem  9879  imadomg  9956  iundom2g  9962  smobeth  10008  canth4  10069  gruina  10240  grur1a  10241  pinn  10300  niex  10303  ltsopi  10310  ltrelpi  10311  dmaddpi  10312  dmmulpi  10313  enqex  10344  ltrelnq  10348  nqerf  10352  nqerrel  10354  dmrecnq  10390  lterpq  10392  ltrelpr  10420  enrex  10489  ltrelsr  10490  dmaddsr  10507  dmmulsr  10508  ltrelre  10556  axaddf  10567  axmulf  10568  ltrelxr  10702  lerelxr  10704  nn0ssre  11902  nn0sscn  11903  nn0ssz  12004  uzsupss  12341  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  fz1ssfz0  13004  uzsup  13232  fzfi  13341  swrd00  14006  sqrlem3  14604  cau3  14715  caubnd  14718  limsupgre  14838  rlimpm  14857  rlimclim  14903  isercolllem1  15021  isercolllem2  15022  isercoll  15024  caurcvg  15033  caucvg  15035  iseraltlem2  15039  iseraltlem3  15040  zsum  15075  fsumcvg3  15086  climfsum  15175  ackbijnn  15183  divcnvshft  15210  infcvgaux1i  15212  clim2prod  15244  ntrivcvg  15253  ntrivcvgfvn0  15255  ntrivcvgtail  15256  ntrivcvgmullem  15257  ntrivcvgmul  15258  zprod  15291  dvdszrcl  15612  4sqlem1  16284  4sqlem19  16299  ramub1lem2  16363  structcnvcnv  16497  fvsetsid  16515  strleun  16591  smndex1sgrp  18073  gicer  18416  symgbasfi  18507  mvdco  18573  symgsssg  18595  efglem  18842  efgtf  18848  efgtlen  18852  efginvrel2  18853  efginvrel1  18854  efgsfo  18865  efgredlemg  18868  efgredleme  18869  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  efgred  18874  efgrelexlemb  18876  efgcpbllemb  18881  frgpinv  18890  frgpuplem  18898  frgpupf  18899  frgpup1  18901  frgpnabllem2  18994  gsumval3lem1  19025  gsumval3lem2  19026  gsumval3  19027  lbsextlem3  19932  ply1bascl  20371  znf1o  20698  zntoslem  20703  pjpm  20852  dmtopon  21531  ordtbas  21800  leordtval2  21820  lecldbas  21827  lmfval  21840  lmbrf  21868  cnconst2  21891  conncompcld  22042  hauspwdom  22109  txuni2  22173  xkouni  22207  xkoccn  22227  txkgen  22260  qtoptop2  22307  kqdisj  22340  hmphtop  22386  hmpher  22392  uzrest  22505  uzfbas  22506  lmflf  22613  tgpconncompeqg  22720  tgpconncomp  22721  ustn0  22829  xmeter  23043  isngp2  23206  xrtgioo  23414  iccntr  23429  xmetdcn  23446  metdcn  23448  metdscn2  23465  icchmeo  23545  cnheiborlem  23558  lmmbrf  23865  iscau4  23882  iscauf  23883  caucfil  23886  lmclimf  23907  volf  24130  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  volcn  24207  mbfimaopnlem  24256  mbflimsup  24267  i1f1  24291  itg2lcl  24328  itgioo  24416  itgsplitioo  24438  limcflflem  24478  limcflf  24479  limcresi  24483  lhop  24613  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlimge0  24627  dvfsumrlim  24628  dvfsumrlim2  24629  dvfsum2  24631  vieta1lem1  24899  vieta1lem2  24900  psercnlem2  25012  psercnlem1  25013  psercn  25014  pserdvlem1  25015  pserdvlem2  25016  pserdv  25017  pserdv2  25018  logcnlem5  25229  dvlog  25234  dvlog2lem  25235  dvlog2  25236  dvcncxp1  25324  dvcnsqrt  25325  cxpcn3lem  25328  cxpcn3  25329  sqrtcn  25331  1cubr  25420  atansssdm  25511  jensen  25566  musum  25768  ppiub  25780  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  2sqlem7  26000  axtgcgrrflx  26248  axtgcgrid  26249  axtgsegcon  26250  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  tglng  26332  disjxwwlkn  27692  frgrwopreg2  28098  phnv  28591  htthlem  28694  hlimadd  28970  hlimcaui  29013  hhsscms  29055  occllem  29080  shjshsi  29269  3oalem4  29442  pjfi  29481  dmadjss  29664  nlelshi  29837  nlelchi  29838  hmopidmchi  29928  shatomistici  30138  difxp1ss  30282  difxp2ss  30283  fcoinver  30357  opabssi  30364  mptctf  30453  fcobijfs  30459  pmtrcnel2  30734  psgnfzto1stlem  30742  cycpmrn  30785  cyc3genpm  30794  lsmsnorb  30945  cnre2csqima  31154  raddcn  31172  rrhre  31262  esumsnf  31323  sxbrsiga  31548  omssubadd  31558  carsggect  31576  sitmcl  31609  oddpwdc  31612  eulerpartlem1  31625  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemmf  31633  eulerpartlemgh  31636  sseqf  31650  ballotlemfmpn  31752  ballotth  31795  signswch  31831  ftc2re  31869  fdvposlt  31870  fdvposle  31872  bnj1146  32063  bnj1292  32087  bnj1293  32088  bnj1145  32265  bnj1177  32278  subfacp1lem3  32429  subfacp1lem5  32431  erdszelem2  32439  kur14lem3  32455  kur14lem6  32458  kur14lem7  32459  kur14lem9  32461  cvmlift2lem12  32561  mpstssv  32786  mstapst  32794  mppspstlem  32818  mppspst  32821  mthmsta  32825  mthmpps  32829  mclsppslem  32830  dfpo2  32991  nosupbnd1lem1  33208  nosupbnd2  33216  scutf  33273  txpss3v  33339  pprodss4v  33345  relsset  33349  fixssdm  33367  fixssrn  33368  limitssson  33372  funpartss  33405  colinearex  33521  fneer  33701  neibastop1  33707  neibastop2lem  33708  filnetlem2  33727  filnetlem3  33728  knoppcnlem10  33841  bj-tagss  34295  bj-fvsnun2  34541  bj-ablssgrp  34561  bj-ablsscmn  34563  bj-vecssmod  34566  bj-flddrng  34573  icoreresf  34636  icoreunrn  34643  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimir  34940  broucube  34941  dvasin  34993  dvacos  34994  areacirc  35002  caures  35050  bnd2lem  35084  ismtyres  35101  flddivrng  35292  xrnss3v  35639  refrelsredund2  35883  toycom  36124  dihglblem2N  38445  lcdvbase  38744  mapdunirnN  38801  prjspreln0  39279  prjspvs  39280  prjspeclsp  39282  0prjspnrel  39289  dffltz  39291  eldiophb  39374  monotuz  39558  pwssplit4  39709  pwfi2f1o  39716  arearect  39842  fvnonrel  39977  rclexi  39995  rtrclex  39997  trclexi  40000  rtrclexi  40001  clcnvlem  40003  cnvrcl0  40005  cnvtrcl0  40006  dfrtrcl5  40009  dfrcl2  40039  comptiunov2i  40071  corclrcl  40072  trclrelexplem  40076  relexpaddss  40083  cotrcltrcl  40090  corcltrcl  40104  cotrclrcl  40107  frege131d  40129  rp-imass  40137  0he  40148  grumnudlem  40641  uzmptshftfval  40698  binomcxplemdvbinom  40705  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  rabexgf  41301  uzct  41345  disjf1o  41472  dmresss  41521  dmmptssf  41522  mptssid  41531  uzfissfz  41614  ssuzfz  41637  uzssre2  41700  uzublem  41724  uzssz2  41752  uzsscn2  41774  sumnnodd  41931  climconstmpt  41959  fnlimfvre  41975  fnlimabslt  41980  limsupvaluz  42009  limsupubuzlem  42013  limsupubuz  42014  limsupequzmpt2  42019  limsupmnfuzlem  42027  limsupre3uzlem  42036  liminfequzmpt2  42092  ibliooicc  42276  stoweidlem44  42349  stoweidlem50  42355  stoweidlem51  42356  stoweidlem52  42357  stoweidlem57  42362  stoweidlem59  42364  fourierdlem16  42428  fourierdlem19  42431  fourierdlem21  42433  fourierdlem22  42434  fourierdlem42  42454  fourierdlem83  42494  fouriersw  42536  salexct  42637  salexct3  42645  salgencntex  42646  salgensscntex  42647  sge0less  42694  sge0fodjrnlem  42718  sge0isum  42729  ovnsslelem  42862  ovnlerp  42864  ovn0lem  42867  hoidmv1lelem1  42893  hoidmv1lelem3  42895  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  ovnhoilem1  42903  ovnhoilem2  42904  opnvonmbllem2  42935  ovolval4lem1  42951  ovolval5lem3  42956  pimdecfgtioc  43013  pimincfltioc  43014  pimdecfgtioo  43015  pimincfltioo  43016  incsmflem  43038  decsmflem  43062  smflimlem2  43068  smflimlem3  43069  smflim  43073  smfrec  43084  smfmullem4  43089  smfdiv  43092  smfsuplem1  43105  smfsuplem3  43107  smfsupxr  43110  smfliminflem  43124  oddibas  44100  2zlidl  44225  2zrngbas  44227  2zrng0  44229  fldc  44374  fldhmsubc  44375  fldcALTV  44392  fldhmsubcALTV  44393  setrec2lem1  44816