Theorem eqsstri 3980

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

Syntax hints:   = wceq 1541   ⊆ wss 3901

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 2708

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

This theorem is referenced by:  eqsstrri  3981  3sstr4i  3985  ssrab3  4034  rabssab  4037  ifssun  4497  opabss  5162  brab2a  5717  relopabiALT  5772  dmopabss  5867  rnopabss  5904  resss  5960  relres  5964  rnin  6104  rnxpss  6130  cnvcnvss  6152  resdmss  6193  resssxp  6228  dfpo2  6254  predss  6267  fnres  6619  f0  6715  nfvres  6872  fvopab4ndm  6971  ffvresb  7070  mptexgf  7168  funiunfv  7194  isoini2  7285  ovssunirn  7394  dmoprabss  7462  mpondm0  7598  elmpocl  7599  exse2  7859  fabexgOLD  7881  frxp  8068  tposssxp  8172  dftpos4  8187  smores  8284  smores2  8286  iordsmo  8289  swoer  8666  swoord1  8667  swoord2  8668  ecss  8686  ecopovsym  8756  ecopovtrn  8757  ecopover  8758  f1setex  8794  sbthlem7  9021  imafi  9215  elfiun  9333  marypha1lem  9336  marypha2lem1  9338  hartogslem1  9447  wdomima2g  9491  inf3lem1  9537  dmttrcl  9630  rnttrcl  9631  tc2  9649  frmin  9661  frrlem16  9670  frr1  9671  tz9.12lem1  9699  rankuni  9775  rankuniss  9778  rankmapu  9790  hta  9809  r0weon  9922  infxpenlem  9923  ackbij1lem9  10137  ackbij1lem10  10138  ackbij1b  10148  sdom2en01  10212  fin23lem26  10235  fin56  10303  fin1a2lem9  10318  axdc3lem  10360  axdc3lem2  10361  axcclem  10367  imadomg  10444  iundom2g  10450  smobeth  10497  canth4  10558  gruina  10729  grur1a  10730  pinn  10789  niex  10792  ltsopi  10799  ltrelpi  10800  dmaddpi  10801  dmmulpi  10802  enqex  10833  ltrelnq  10837  nqerf  10841  nqerrel  10843  dmrecnq  10879  lterpq  10881  ltrelpr  10909  enrex  10978  ltrelsr  10979  dmaddsr  10996  dmmulsr  10997  ltrelre  11045  axaddf  11056  axmulf  11057  ltrelxr  11193  lerelxr  11195  nn0ssre  12405  nn0sscn  12406  nn0ssz  12511  uzsupss  12853  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  fz1ssfz0  13539  uzsup  13783  fzfi  13895  swrd00  14568  01sqrexlem3  15167  cau3  15279  caubnd  15282  limsupgre  15404  rlimpm  15423  rlimclim  15469  isercolllem1  15588  isercolllem2  15589  isercoll  15591  caurcvg  15600  caucvg  15602  iseraltlem2  15606  iseraltlem3  15607  zsum  15641  fsumcvg3  15652  climfsum  15743  ackbijnn  15751  divcnvshft  15778  infcvgaux1i  15780  clim2prod  15811  ntrivcvg  15820  ntrivcvgfvn0  15822  ntrivcvgtail  15823  ntrivcvgmullem  15824  ntrivcvgmul  15825  zprod  15860  dvdszrcl  16184  4sqlem1  16876  4sqlem19  16891  ramub1lem2  16955  structcnvcnv  17080  strleun  17084  fvsetsid  17095  smndex1sgrp  18833  gicer  19206  cntzsgrpcl  19263  symgbasfi  19308  mvdco  19374  symgsssg  19396  efglem  19645  efgtf  19651  efgtlen  19655  efginvrel2  19656  efginvrel1  19657  efgsfo  19668  efgredlemg  19671  efgredleme  19672  efgredlemd  19673  efgredlemc  19674  efgredlem  19676  efgred  19677  efgrelexlemb  19679  efgcpbllemb  19684  frgpinv  19693  frgpuplem  19701  frgpupf  19702  frgpup1  19704  frgpnabllem2  19803  gsumval3lem1  19834  gsumval3lem2  19835  gsumval3  19836  fldc  20717  fldhmsubc  20718  lbsextlem3  21115  pzriprnglem10  21445  znf1o  21506  zntoslem  21511  pjpm  21663  mhp0cl  22089  ply1bascl  22144  dmtopon  22867  ordtbas  23136  leordtval2  23156  lecldbas  23163  lmfval  23176  lmbrf  23204  cnconst2  23227  conncompcld  23378  hauspwdom  23445  txuni2  23509  xkouni  23543  xkoccn  23563  txkgen  23596  qtoptop2  23643  kqdisj  23676  hmphtop  23722  hmpher  23728  uzrest  23841  uzfbas  23842  lmflf  23949  tgpconncompeqg  24056  tgpconncomp  24057  ustn0  24165  xmeter  24377  isngp2  24541  xrtgioo  24751  iccntr  24766  xmetdcn  24783  metdcn  24785  metdscn2  24802  icchmeoOLD  24895  cnheiborlem  24909  reparphti  24952  lmmbrf  25218  iscau4  25235  iscauf  25236  caucfil  25239  lmclimf  25260  volf  25486  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  volcn  25563  mbfimaopnlem  25612  mbflimsup  25623  i1f1  25647  itg2lcl  25684  itgioo  25773  itgsplitioo  25795  limcflflem  25837  limcflf  25838  limcresi  25842  lhop  25977  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsumrlimge0  25993  dvfsumrlim  25994  dvfsumrlim2  25995  dvfsum2  25997  vieta1lem1  26274  vieta1lem2  26275  psercnlem2  26390  psercnlem1  26391  psercn  26392  pserdvlem1  26393  pserdvlem2  26394  pserdv  26395  pserdv2  26396  logcnlem5  26611  dvlog  26616  dvlog2lem  26617  dvlog2  26618  dvcncxp1  26708  dvcnsqrt  26709  cxpcn3lem  26713  cxpcn3  26714  sqrtcn  26716  1cubr  26808  atansssdm  26899  jensen  26955  musum  27157  ppiub  27171  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  2sqlem7  27391  nosupbnd1lem1  27676  nosupbnd2  27684  noinfbnd1lem1  27691  cutsf  27788  leftssold  27867  rightssold  27868  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  precsexlem8  28210  onssno  28250  nnssn0s  28317  dfnns2  28368  bdaypw2n0bndlem  28459  axtgcgrrflx  28534  axtgcgrid  28535  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgcont1  28540  tglng  28618  disjxwwlkn  29986  frgrwopreg2  30394  phnv  30889  htthlem  30992  hlimadd  31268  hlimcaui  31311  hhsscms  31353  occllem  31378  shjshsi  31567  3oalem4  31740  pjfi  31779  dmadjss  31962  nlelshi  32135  nlelchi  32136  hmopidmchi  32226  shatomistici  32436  difxp1ss  32597  difxp2ss  32598  fcoinver  32679  opabssi  32691  mptctf  32795  ccatws1f1o  33033  gsumpart  33146  pmtrcnel2  33172  psgnfzto1stlem  33182  cycpmrn  33225  cyc3genpm  33234  unitprodclb  33470  lsmsnorb  33472  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  evlextv  33707  vietalem  33735  constrsscn  33897  cnre2csqima  34068  raddcn  34086  zrhcntr  34136  rrhre  34178  esumsnf  34221  sxbrsiga  34447  omssubadd  34457  carsggect  34475  sitmcl  34508  oddpwdc  34511  eulerpartlem1  34524  eulerpartlemt  34528  eulerpartgbij  34529  eulerpartlemmf  34532  eulerpartlemgh  34535  sseqf  34549  ballotlemfmpn  34652  ballotth  34695  signswch  34718  ftc2re  34755  fdvposlt  34756  fdvposle  34758  bnj1146  34947  bnj1292  34971  bnj1293  34972  bnj1145  35149  bnj1177  35162  fineqvnttrclse  35280  tz9.1regs  35290  erdszelem2  35386  kur14lem3  35402  kur14lem6  35405  kur14lem7  35406  kur14lem9  35408  cvmlift2lem12  35508  mpstssv  35733  mstapst  35741  mppspstlem  35765  mppspst  35768  mthmsta  35772  mthmpps  35776  mclsppslem  35777  txpss3v  36070  pprodss4v  36076  relsset  36080  fixssdm  36098  fixssrn  36099  limitssson  36103  funpartss  36138  colinearex  36254  fneer  36547  neibastop1  36553  neibastop2lem  36554  filnetlem2  36573  filnetlem3  36574  knoppcnlem10  36702  bj-tagss  37181  bj-imdirco  37395  bj-fvsnun2  37461  bj-ablssgrp  37481  bj-ablsscmn  37483  bj-vecssmod  37486  bj-fldssdrng  37493  icoreresf  37557  icoreunrn  37564  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimir  37854  broucube  37855  dvasin  37905  dvacos  37906  areacirc  37914  caures  37961  bnd2lem  37992  ismtyres  38009  flddivrng  38200  xrnss3v  38566  refrelsredund2  38890  toycom  39233  dihglblem2N  41554  lcdvbase  41853  mapdunirnN  41910  aks6d1c1p1rcl  42362  redvmptabs  42615  readvrec  42617  prjspreln0  42852  prjspvs  42853  prjspeclsp  42855  0prjspnrel  42870  dffltz  42877  eldiophb  42999  monotuz  43183  pwssplit4  43331  pwfi2f1o  43338  arearect  43457  cantnfresb  43566  omabs2  43574  fvnonrel  43838  rclexi  43856  rtrclex  43858  trclexi  43861  rtrclexi  43862  clcnvlem  43864  cnvrcl0  43866  cnvtrcl0  43867  dfrtrcl5  43870  dfrcl2  43915  comptiunov2i  43947  corclrcl  43948  trclrelexplem  43952  relexpaddss  43959  cotrcltrcl  43966  corcltrcl  43980  cotrclrcl  43983  frege131d  44005  0he  44023  grumnudlem  44526  uzmptshftfval  44587  binomcxplemdvbinom  44594  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  modelaxreplem2  45220  rabexgf  45269  uzct  45308  disjf1o  45435  dmmptssf  45476  mptssid  45485  uzfissfz  45571  ssuzfz  45594  uzssre2  45651  uzublem  45674  uzssz2  45700  uzsscn2  45721  sumnnodd  45876  climconstmpt  45902  fnlimfvre  45918  fnlimabslt  45923  limsupvaluz  45952  limsupubuzlem  45956  limsupubuz  45957  limsupequzmpt2  45962  limsupmnfuzlem  45970  limsupre3uzlem  45979  liminfequzmpt2  46035  ibliooicc  46215  stoweidlem44  46288  stoweidlem50  46294  stoweidlem51  46295  stoweidlem52  46296  stoweidlem57  46301  stoweidlem59  46303  fourierdlem16  46367  fourierdlem19  46370  fourierdlem21  46372  fourierdlem22  46373  fourierdlem42  46393  fourierdlem83  46433  fouriersw  46475  salexct  46578  salexct3  46586  salgencntex  46587  salgensscntex  46588  sge0less  46636  sge0fodjrnlem  46660  sge0isum  46671  ovnlerp  46806  ovn0lem  46809  hoidmv1lelem1  46835  hoidmv1lelem3  46837  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  ovnhoilem1  46845  ovnhoilem2  46846  opnvonmbllem2  46877  ovolval4lem1  46893  ovolval5lem3  46898  pimdecfgtioc  46959  pimincfltioc  46960  pimdecfgtioo  46961  pimincfltioo  46962  incsmflem  46985  decsmflem  47010  smflimlem2  47016  smflimlem3  47017  smflim  47021  smfrec  47033  smfmullem4  47038  smfdiv  47041  smfsuplem1  47055  smfsuplem3  47057  smfsupxr  47060  smfliminflem  47074  cfsetssfset  47302  fcoreslem2  47310  fcores  47313  gricrel  48165  clnbgrisubgrgrim  48178  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  isubgr3stgrlem8  48219  isubgr3stgr  48221  grlimgrtrilem2  48248  grlicrel  48252  oddibas  48419  2zlidl  48486  2zrngbas  48488  2zrng0  48490  fldcALTV  48578  fldhmsubcALTV  48579  dmtposss  49121  tposres3  49126  ipolub0  49237  imaidfu  49355