Theorem eqsstri 3969

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

Syntax hints:   = wceq 1542   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqsstrri  3970  3sstr4i  3974  ssrab3  4023  rabssab  4026  ifssun  4485  opabss  5150  brab2a  5719  relopabiALT  5774  dmopabss  5869  rnopabss  5906  resss  5962  relres  5966  rnin  6106  rnxpss  6132  cnvcnvss  6154  resdmss  6195  resssxp  6230  dfpo2  6256  predss  6269  fnres  6621  f0  6717  nfvres  6874  fvopab4ndm  6974  ffvresb  7074  mptexgf  7172  funiunfv  7198  isoini2  7289  ovssunirn  7398  dmoprabss  7466  mpondm0  7602  elmpocl  7603  exse2  7863  fabexgOLD  7885  frxp  8071  tposssxp  8175  dftpos4  8190  smores  8287  smores2  8289  iordsmo  8292  swoer  8670  swoord1  8671  swoord2  8672  ecss  8690  ecopovsym  8761  ecopovtrn  8762  ecopover  8763  f1setex  8799  sbthlem7  9026  imafi  9220  elfiun  9338  marypha1lem  9341  marypha2lem1  9343  hartogslem1  9452  wdomima2g  9496  inf3lem1  9544  dmttrcl  9637  rnttrcl  9638  tc2  9656  frmin  9668  frrlem16  9677  frr1  9678  tz9.12lem1  9706  rankuni  9782  rankuniss  9785  rankmapu  9797  hta  9816  r0weon  9929  infxpenlem  9930  ackbij1lem9  10144  ackbij1lem10  10145  ackbij1b  10155  sdom2en01  10219  fin23lem26  10242  fin56  10310  fin1a2lem9  10325  axdc3lem  10367  axdc3lem2  10368  axcclem  10374  imadomg  10451  iundom2g  10457  smobeth  10504  canth4  10565  gruina  10736  grur1a  10737  pinn  10796  niex  10799  ltsopi  10806  ltrelpi  10807  dmaddpi  10808  dmmulpi  10809  enqex  10840  ltrelnq  10844  nqerf  10848  nqerrel  10850  dmrecnq  10886  lterpq  10888  ltrelpr  10916  enrex  10985  ltrelsr  10986  dmaddsr  11003  dmmulsr  11004  ltrelre  11052  axaddf  11063  axmulf  11064  ltrelxr  11201  lerelxr  11203  nn0ssre  12436  nn0sscn  12437  nn0ssz  12542  uzsupss  12885  rpnnen1lem1  12923  rpnnen1lem3  12924  rpnnen1lem5  12926  fz1ssfz0  13572  uzsup  13817  fzfi  13929  swrd00  14602  01sqrexlem3  15201  cau3  15313  caubnd  15316  limsupgre  15438  rlimpm  15457  rlimclim  15503  isercolllem1  15622  isercolllem2  15623  isercoll  15625  caurcvg  15634  caucvg  15636  iseraltlem2  15640  iseraltlem3  15641  zsum  15675  fsumcvg3  15686  climfsum  15778  ackbijnn  15788  divcnvshft  15815  infcvgaux1i  15817  clim2prod  15848  ntrivcvg  15857  ntrivcvgfvn0  15859  ntrivcvgtail  15860  ntrivcvgmullem  15861  ntrivcvgmul  15862  zprod  15897  dvdszrcl  16221  4sqlem1  16914  4sqlem19  16929  ramub1lem2  16993  structcnvcnv  17118  strleun  17122  fvsetsid  17133  smndex1sgrp  18874  gicer  19247  cntzsgrpcl  19304  symgbasfi  19349  mvdco  19415  symgsssg  19437  efglem  19686  efgtf  19692  efgtlen  19696  efginvrel2  19697  efginvrel1  19698  efgsfo  19709  efgredlemg  19712  efgredleme  19713  efgredlemd  19714  efgredlemc  19715  efgredlem  19717  efgred  19718  efgrelexlemb  19720  efgcpbllemb  19725  frgpinv  19734  frgpuplem  19742  frgpupf  19743  frgpup1  19745  frgpnabllem2  19844  gsumval3lem1  19875  gsumval3lem2  19876  gsumval3  19877  fldc  20756  fldhmsubc  20757  lbsextlem3  21154  pzriprnglem10  21484  znf1o  21545  zntoslem  21550  pjpm  21702  mhp0cl  22126  ply1bascl  22181  dmtopon  22902  ordtbas  23171  leordtval2  23191  lecldbas  23198  lmfval  23211  lmbrf  23239  cnconst2  23262  conncompcld  23413  hauspwdom  23480  txuni2  23544  xkouni  23578  xkoccn  23598  txkgen  23631  qtoptop2  23678  kqdisj  23711  hmphtop  23757  hmpher  23763  uzrest  23876  uzfbas  23877  lmflf  23984  tgpconncompeqg  24091  tgpconncomp  24092  ustn0  24200  xmeter  24412  isngp2  24576  xrtgioo  24786  iccntr  24801  xmetdcn  24818  metdcn  24820  metdscn2  24837  cnheiborlem  24935  reparphti  24978  lmmbrf  25243  iscau4  25260  iscauf  25261  caucfil  25264  lmclimf  25285  volf  25510  uniioombllem3  25566  uniioombllem4  25567  uniioombllem5  25568  volcn  25587  mbfimaopnlem  25636  mbflimsup  25647  i1f1  25671  itg2lcl  25708  itgioo  25797  itgsplitioo  25819  limcflflem  25861  limcflf  25862  limcresi  25866  lhop  25997  dvfsumlem1  26007  dvfsumlem2  26008  dvfsumlem3  26009  dvfsumlem4  26010  dvfsumrlimge0  26011  dvfsumrlim  26012  dvfsumrlim2  26013  dvfsum2  26015  vieta1lem1  26291  vieta1lem2  26292  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  pserdv  26411  pserdv2  26412  logcnlem5  26627  dvlog  26632  dvlog2lem  26633  dvlog2  26634  dvcncxp1  26724  dvcnsqrt  26725  cxpcn3lem  26728  cxpcn3  26729  sqrtcn  26731  1cubr  26823  atansssdm  26914  jensen  26970  musum  27172  ppiub  27185  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  2sqlem7  27405  nosupbnd1lem1  27690  nosupbnd2  27698  noinfbnd1lem1  27705  cutsf  27802  leftssold  27881  rightssold  27882  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  precsexlem8  28224  onssno  28264  nnssn0s  28331  dfnns2  28382  bdaypw2n0bndlem  28473  axtgcgrrflx  28548  axtgcgrid  28549  axtgsegcon  28550  axtg5seg  28551  axtgbtwnid  28552  axtgpasch  28553  axtgcont1  28554  tglng  28632  disjxwwlkn  30000  frgrwopreg2  30408  phnv  30904  htthlem  31007  hlimadd  31283  hlimcaui  31326  hhsscms  31368  occllem  31393  shjshsi  31582  3oalem4  31755  pjfi  31794  dmadjss  31977  nlelshi  32150  nlelchi  32151  hmopidmchi  32241  shatomistici  32451  difxp1ss  32611  difxp2ss  32612  fcoinver  32693  opabssi  32705  mptctf  32808  ccatws1f1o  33030  gsumpart  33143  pmtrcnel2  33170  psgnfzto1stlem  33180  cycpmrn  33223  cyc3genpm  33232  unitprodclb  33468  lsmsnorb  33470  ply1degltel  33673  ply1degleel  33674  ply1degltlss  33675  evlextv  33705  vietalem  33742  constrsscn  33904  cnre2csqima  34075  raddcn  34093  zrhcntr  34143  rrhre  34185  esumsnf  34228  sxbrsiga  34454  omssubadd  34464  carsggect  34482  sitmcl  34515  oddpwdc  34518  eulerpartlem1  34531  eulerpartlemt  34535  eulerpartgbij  34536  eulerpartlemmf  34539  eulerpartlemgh  34542  sseqf  34556  ballotlemfmpn  34659  ballotth  34702  signswch  34725  ftc2re  34762  fdvposlt  34763  fdvposle  34765  bnj1146  34953  bnj1292  34977  bnj1293  34978  bnj1145  35155  bnj1177  35168  fineqvnttrclse  35288  tz9.1regs  35298  erdszelem2  35394  kur14lem3  35410  kur14lem6  35413  kur14lem7  35414  kur14lem9  35416  cvmlift2lem12  35516  mpstssv  35741  mstapst  35749  mppspstlem  35773  mppspst  35776  mthmsta  35780  mthmpps  35784  mclsppslem  35785  txpss3v  36078  pprodss4v  36084  relsset  36088  fixssdm  36106  fixssrn  36107  limitssson  36111  funpartss  36146  colinearex  36262  fneer  36555  neibastop1  36561  neibastop2lem  36562  filnetlem2  36581  filnetlem3  36582  ttcuniun  36712  ttcuni  36715  knoppcnlem10  36782  bj-tagss  37307  bj-imdirco  37524  bj-fvsnun2  37590  bj-ablssgrp  37610  bj-ablsscmn  37612  bj-vecssmod  37615  bj-fldssdrng  37622  icoreresf  37686  icoreunrn  37693  poimirlem29  37988  poimirlem30  37989  poimirlem31  37990  poimir  37992  broucube  37993  dvasin  38043  dvacos  38044  areacirc  38052  caures  38099  bnd2lem  38130  ismtyres  38147  flddivrng  38338  xrnss3v  38720  refrelsredund2  39056  toycom  39437  dihglblem2N  41758  lcdvbase  42057  mapdunirnN  42114  aks6d1c1p1rcl  42565  redvmptabs  42810  readvrec  42812  prjspreln0  43060  prjspvs  43061  prjspeclsp  43063  0prjspnrel  43078  dffltz  43085  eldiophb  43207  monotuz  43391  pwssplit4  43539  pwfi2f1o  43546  arearect  43665  cantnfresb  43774  omabs2  43782  fvnonrel  44046  rclexi  44064  rtrclex  44066  trclexi  44069  rtrclexi  44070  clcnvlem  44072  cnvrcl0  44074  cnvtrcl0  44075  dfrtrcl5  44078  dfrcl2  44123  comptiunov2i  44155  corclrcl  44156  trclrelexplem  44160  relexpaddss  44167  cotrcltrcl  44174  corcltrcl  44188  cotrclrcl  44191  frege131d  44213  0he  44231  grumnudlem  44734  uzmptshftfval  44795  binomcxplemdvbinom  44802  binomcxplemdvsum  44804  binomcxplemnotnn0  44805  modelaxreplem2  45428  rabexgf  45477  uzct  45516  disjf1o  45643  dmmptssf  45683  mptssid  45692  uzfissfz  45778  ssuzfz  45801  uzssre2  45857  uzublem  45880  uzssz2  45906  uzsscn2  45927  sumnnodd  46082  climconstmpt  46108  fnlimfvre  46124  fnlimabslt  46129  limsupvaluz  46158  limsupubuzlem  46162  limsupubuz  46163  limsupequzmpt2  46168  limsupmnfuzlem  46176  limsupre3uzlem  46185  liminfequzmpt2  46241  ibliooicc  46421  stoweidlem44  46494  stoweidlem50  46500  stoweidlem51  46501  stoweidlem52  46502  stoweidlem57  46507  stoweidlem59  46509  fourierdlem16  46573  fourierdlem19  46576  fourierdlem21  46578  fourierdlem22  46579  fourierdlem42  46599  fourierdlem83  46639  fouriersw  46681  salexct  46784  salexct3  46792  salgencntex  46793  salgensscntex  46794  sge0less  46842  sge0fodjrnlem  46866  sge0isum  46877  ovnlerp  47012  ovn0lem  47015  hoidmv1lelem1  47041  hoidmv1lelem3  47043  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  ovnhoilem1  47051  ovnhoilem2  47052  opnvonmbllem2  47083  ovolval4lem1  47099  ovolval5lem3  47104  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  incsmflem  47191  decsmflem  47216  smflimlem2  47222  smflimlem3  47223  smflim  47227  smfrec  47239  smfmullem4  47244  smfdiv  47247  smfsuplem1  47261  smfsuplem3  47263  smfsupxr  47266  smfliminflem  47280  cfsetssfset  47520  fcoreslem2  47528  fcores  47531  gricrel  48411  clnbgrisubgrgrim  48424  isubgr3stgrlem6  48463  isubgr3stgrlem7  48464  isubgr3stgrlem8  48465  isubgr3stgr  48467  grlimgrtrilem2  48494  grlicrel  48498  oddibas  48665  2zlidl  48732  2zrngbas  48734  2zrng0  48736  fldcALTV  48824  fldhmsubcALTV  48825  dmtposss  49367  tposres3  49372  ipolub0  49483  imaidfu  49601