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 1542   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  eqsstrri  4017  ssrab2OLD  4078  ssrab3  4080  rabssab  4083  ifssun  4545  opabss  5212  brab2a  5768  relopabiALT  5822  dmopabss  5917  resss  6005  relres  6009  rnin  6144  rnxpss  6169  cnvcnvss  6191  resdmss  6232  resssxp  6267  dfpo2  6293  predss  6306  fnres  6675  f0  6770  nfvres  6930  fvopab4ndm  7025  ffvresb  7121  mptexgf  7221  funiunfv  7244  isoini2  7333  ovssunirn  7442  dmoprabss  7508  mpondm0  7644  elmpocl  7645  exse2  7905  fabexg  7922  frxp  8109  tposssxp  8212  dftpos4  8227  wfrdmssOLD  8312  smores  8349  smores2  8351  iordsmo  8354  swoer  8730  swoord1  8731  swoord2  8732  ecss  8746  ecopovsym  8810  ecopovtrn  8811  ecopover  8812  f1setex  8848  sbthlem7  9086  nnfiOLD  9229  imafiALT  9342  elfiun  9422  marypha1lem  9425  marypha2lem1  9427  hartogslem1  9534  wdomima2g  9578  inf3lem1  9620  dmttrcl  9713  rnttrcl  9714  tc2  9734  frmin  9741  frrlem16  9750  frr1  9751  tz9.12lem1  9779  rankuni  9855  rankuniss  9858  rankmapu  9870  hta  9889  r0weon  10004  infxpenlem  10005  ackbij1lem9  10220  ackbij1lem10  10221  ackbij1b  10231  sdom2en01  10294  fin23lem26  10317  fin56  10385  fin1a2lem9  10400  axdc3lem  10442  axdc3lem2  10443  axcclem  10449  imadomg  10526  iundom2g  10532  smobeth  10578  canth4  10639  gruina  10810  grur1a  10811  pinn  10870  niex  10873  ltsopi  10880  ltrelpi  10881  dmaddpi  10882  dmmulpi  10883  enqex  10914  ltrelnq  10918  nqerf  10922  nqerrel  10924  dmrecnq  10960  lterpq  10962  ltrelpr  10990  enrex  11059  ltrelsr  11060  dmaddsr  11077  dmmulsr  11078  ltrelre  11126  axaddf  11137  axmulf  11138  ltrelxr  11272  lerelxr  11274  nn0ssre  12473  nn0sscn  12474  nn0ssz  12578  uzsupss  12921  rpnnen1lem1  12959  rpnnen1lem3  12960  rpnnen1lem5  12962  fz1ssfz0  13594  uzsup  13825  fzfi  13934  swrd00  14591  01sqrexlem3  15188  cau3  15299  caubnd  15302  limsupgre  15422  rlimpm  15441  rlimclim  15487  isercolllem1  15608  isercolllem2  15609  isercoll  15611  caurcvg  15620  caucvg  15622  iseraltlem2  15626  iseraltlem3  15627  zsum  15661  fsumcvg3  15672  climfsum  15763  ackbijnn  15771  divcnvshft  15798  infcvgaux1i  15800  clim2prod  15831  ntrivcvg  15840  ntrivcvgfvn0  15842  ntrivcvgtail  15843  ntrivcvgmullem  15844  ntrivcvgmul  15845  zprod  15878  dvdszrcl  16199  4sqlem1  16878  4sqlem19  16893  ramub1lem2  16957  structcnvcnv  17083  strleun  17087  fvsetsid  17098  smndex1sgrp  18786  gicer  19145  cntzsgrpcl  19193  symgbasfi  19241  mvdco  19308  symgsssg  19330  efglem  19579  efgtf  19585  efgtlen  19589  efginvrel2  19590  efginvrel1  19591  efgsfo  19602  efgredlemg  19605  efgredleme  19606  efgredlemd  19607  efgredlemc  19608  efgredlem  19610  efgred  19611  efgrelexlemb  19613  efgcpbllemb  19618  frgpinv  19627  frgpuplem  19635  frgpupf  19636  frgpup1  19638  frgpnabllem2  19737  gsumval3lem1  19768  gsumval3lem2  19769  gsumval3  19770  lbsextlem3  20766  znf1o  21099  zntoslem  21104  pjpm  21255  mhp0cl  21681  ply1bascl  21719  dmtopon  22417  ordtbas  22688  leordtval2  22708  lecldbas  22715  lmfval  22728  lmbrf  22756  cnconst2  22779  conncompcld  22930  hauspwdom  22997  txuni2  23061  xkouni  23095  xkoccn  23115  txkgen  23148  qtoptop2  23195  kqdisj  23228  hmphtop  23274  hmpher  23280  uzrest  23393  uzfbas  23394  lmflf  23501  tgpconncompeqg  23608  tgpconncomp  23609  ustn0  23717  xmeter  23931  isngp2  24098  xrtgioo  24314  iccntr  24329  xmetdcn  24346  metdcn  24348  metdscn2  24365  icchmeo  24449  cnheiborlem  24462  lmmbrf  24771  iscau4  24788  iscauf  24789  caucfil  24792  lmclimf  24813  volf  25038  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  volcn  25115  mbfimaopnlem  25164  mbflimsup  25175  i1f1  25199  itg2lcl  25237  itgioo  25325  itgsplitioo  25347  limcflflem  25389  limcflf  25390  limcresi  25394  lhop  25525  dvfsumlem1  25535  dvfsumlem2  25536  dvfsumlem3  25537  dvfsumlem4  25538  dvfsumrlimge0  25539  dvfsumrlim  25540  dvfsumrlim2  25541  dvfsum2  25543  vieta1lem1  25815  vieta1lem2  25816  psercnlem2  25928  psercnlem1  25929  psercn  25930  pserdvlem1  25931  pserdvlem2  25932  pserdv  25933  pserdv2  25934  logcnlem5  26146  dvlog  26151  dvlog2lem  26152  dvlog2  26153  dvcncxp1  26241  dvcnsqrt  26242  cxpcn3lem  26245  cxpcn3  26246  sqrtcn  26248  1cubr  26337  atansssdm  26428  jensen  26483  musum  26685  ppiub  26697  lgsquadlem1  26873  lgsquadlem2  26874  lgsquadlem3  26875  2sqlem7  26917  nosupbnd1lem1  27201  nosupbnd2  27209  noinfbnd1lem1  27216  scutf  27303  leftssold  27363  rightssold  27364  mulsproplem12  27573  mulsproplem13  27574  mulsproplem14  27575  precsexlem8  27650  axtgcgrrflx  27703  axtgcgrid  27704  axtgsegcon  27705  axtg5seg  27706  axtgbtwnid  27707  axtgpasch  27708  axtgcont1  27709  tglng  27787  disjxwwlkn  29157  frgrwopreg2  29562  phnv  30055  htthlem  30158  hlimadd  30434  hlimcaui  30477  hhsscms  30519  occllem  30544  shjshsi  30733  3oalem4  30906  pjfi  30945  dmadjss  31128  nlelshi  31301  nlelchi  31302  hmopidmchi  31392  shatomistici  31602  difxp1ss  31748  difxp2ss  31749  fcoinver  31823  opabssi  31830  mptctf  31930  gsumpart  32195  pmtrcnel2  32239  psgnfzto1stlem  32247  cycpmrn  32290  cyc3genpm  32299  lsmsnorb  32490  ply1degltel  32655  ply1degltlss  32656  cnre2csqima  32880  raddcn  32898  rrhre  32990  esumsnf  33051  sxbrsiga  33278  omssubadd  33288  carsggect  33306  sitmcl  33339  oddpwdc  33342  eulerpartlem1  33355  eulerpartlemt  33359  eulerpartgbij  33360  eulerpartlemmf  33363  eulerpartlemgh  33366  sseqf  33380  ballotlemfmpn  33482  ballotth  33525  signswch  33561  ftc2re  33599  fdvposlt  33600  fdvposle  33602  bnj1146  33791  bnj1292  33815  bnj1293  33816  bnj1145  33993  bnj1177  34006  erdszelem2  34172  kur14lem3  34188  kur14lem6  34191  kur14lem7  34192  kur14lem9  34194  cvmlift2lem12  34294  mpstssv  34519  mstapst  34527  mppspstlem  34551  mppspst  34554  mthmsta  34558  mthmpps  34562  mclsppslem  34563  txpss3v  34839  pprodss4v  34845  relsset  34849  fixssdm  34867  fixssrn  34868  limitssson  34872  funpartss  34905  colinearex  35021  gg-reparphti  35161  gg-dvfsumlem2  35172  fneer  35227  neibastop1  35233  neibastop2lem  35234  filnetlem2  35253  filnetlem3  35254  knoppcnlem10  35367  bj-tagss  35850  bj-imdirco  36060  bj-fvsnun2  36126  bj-ablssgrp  36146  bj-ablsscmn  36148  bj-vecssmod  36151  bj-fldssdrng  36158  icoreresf  36222  icoreunrn  36229  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimir  36510  broucube  36511  dvasin  36561  dvacos  36562  areacirc  36570  caures  36617  bnd2lem  36648  ismtyres  36665  flddivrng  36856  xrnss3v  37231  refrelsredund2  37492  toycom  37832  dihglblem2N  40154  lcdvbase  40453  mapdunirnN  40510  prjspreln0  41348  prjspvs  41349  prjspeclsp  41351  0prjspnrel  41366  dffltz  41373  eldiophb  41481  monotuz  41666  pwssplit4  41817  pwfi2f1o  41824  arearect  41950  cantnfresb  42060  omabs2  42068  fvnonrel  42334  rclexi  42352  rtrclex  42354  trclexi  42357  rtrclexi  42358  clcnvlem  42360  cnvrcl0  42362  cnvtrcl0  42363  dfrtrcl5  42366  dfrcl2  42411  comptiunov2i  42443  corclrcl  42444  trclrelexplem  42448  relexpaddss  42455  cotrcltrcl  42462  corcltrcl  42476  cotrclrcl  42479  frege131d  42501  0he  42519  grumnudlem  43030  uzmptshftfval  43091  binomcxplemdvbinom  43098  binomcxplemdvsum  43100  binomcxplemnotnn0  43101  rabexgf  43694  uzct  43736  disjf1o  43875  dmresss  43919  dmmptssf  43920  mptssid  43930  uzfissfz  44023  ssuzfz  44046  uzssre2  44104  uzublem  44127  uzssz2  44153  uzsscn2  44175  sumnnodd  44333  climconstmpt  44361  fnlimfvre  44377  fnlimabslt  44382  limsupvaluz  44411  limsupubuzlem  44415  limsupubuz  44416  limsupequzmpt2  44421  limsupmnfuzlem  44429  limsupre3uzlem  44438  liminfequzmpt2  44494  ibliooicc  44674  stoweidlem44  44747  stoweidlem50  44753  stoweidlem51  44754  stoweidlem52  44755  stoweidlem57  44760  stoweidlem59  44762  fourierdlem16  44826  fourierdlem19  44829  fourierdlem21  44831  fourierdlem22  44832  fourierdlem42  44852  fourierdlem83  44892  fouriersw  44934  salexct  45037  salexct3  45045  salgencntex  45046  salgensscntex  45047  sge0less  45095  sge0fodjrnlem  45119  sge0isum  45130  ovnlerp  45265  ovn0lem  45268  hoidmv1lelem1  45294  hoidmv1lelem3  45296  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  ovnhoilem1  45304  ovnhoilem2  45305  opnvonmbllem2  45336  ovolval4lem1  45352  ovolval5lem3  45357  pimdecfgtioc  45418  pimincfltioc  45419  pimdecfgtioo  45420  pimincfltioo  45421  incsmflem  45444  decsmflem  45469  smflimlem2  45475  smflimlem3  45476  smflim  45480  smfrec  45492  smfmullem4  45497  smfdiv  45500  smfsuplem1  45514  smfsuplem3  45516  smfsupxr  45519  smfliminflem  45533  cfsetssfset  45753  fcoreslem2  45761  fcores  45764  oddibas  46570  2zlidl  46786  2zrngbas  46788  2zrng0  46790  fldc  46935  fldhmsubc  46936  fldcALTV  46953  fldhmsubcALTV  46954  ipolub0  47571