Theorem eqsstri 3991

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

Syntax hints:   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqsstrri  3992  3sstr4i  3996  ssrab3  4044  rabssab  4047  ifssun  4510  opabss  5179  brab2a  5755  relopabiALT  5811  dmopabss  5909  rnopabss  5946  resss  6001  relres  6005  rninOLD  6145  rnxpss  6171  cnvcnvss  6193  cnvcnvssOLD  6194  resdmss  6237  resssxp  6272  dfpo2  6298  predss  6311  fnres  6663  f0  6760  nfvres  6920  fvopab4ndm  7021  ffvresb  7122  mptexgf  7221  funiunfv  7247  isoini2  7338  ovssunirn  7447  dmoprabss  7515  mpondm0  7651  elmpocl  7652  exse2  7914  frxp  8122  tposssxp  8226  dftpos4  8241  smores  8339  smores2  8341  iordsmo  8344  swoer  8726  swoord1  8727  swoord2  8728  ecss  8746  ecopovsym  8817  ecopovtrn  8818  ecopover  8819  f1setex  8854  sbthlem7  9081  imafi  9275  elfiun  9390  marypha1lem  9393  marypha2lem1  9395  hartogslem1  9504  wdomima2g  9548  inf3lem1  9597  dmttrcl  9690  rnttrcl  9691  tc2  9709  frmin  9721  frrlem16  9730  frr1  9731  tz9.12lem1  9759  rankuni  9835  rankuniss  9838  rankmapu  9850  hta  9883  r0weon  9996  infxpenlem  9997  ackbij1lem9  10210  ackbij1lem10  10211  ackbij1b  10221  sdom2en01  10286  fin23lem26  10309  fin56  10377  fin1a2lem9  10392  axdc3lem  10434  axdc3lem2  10435  axcclem  10441  imadomg  10518  iundom2g  10524  smobeth  10571  canth4  10632  gruina  10803  grur1a  10804  pinn  10863  niex  10866  ltsopi  10873  ltrelpi  10874  dmaddpi  10875  dmmulpi  10876  enqex  10907  ltrelnq  10911  nqerf  10915  nqerrel  10917  dmrecnq  10953  lterpq  10955  ltrelpr  10983  enrex  11052  ltrelsr  11053  dmaddsr  11070  dmmulsr  11071  ltrelre  11119  axaddf  11130  axmulf  11131  ltrelxr  11270  lerelxr  11272  nn0ssre  12508  nn0sscn  12509  nn0ssz  12614  uzsupss  12964  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  fz1ssfz0  13651  uzsup  13896  fzfi  14008  swrd00  14682  01sqrexlem3  15295  cau3  15407  caubnd  15410  limsupgre  15532  rlimpm  15551  rlimclim  15597  isercolllem1  15716  isercolllem2  15717  isercoll  15719  caurcvg  15728  caucvg  15730  iseraltlem2  15734  iseraltlem3  15735  zsum  15769  fsumcvg3  15780  climfsum  15872  ackbijnn  15882  divcnvshft  15909  infcvgaux1i  15911  clim2prod  15942  ntrivcvg  15951  ntrivcvgfvn0  15953  ntrivcvgtail  15954  ntrivcvgmullem  15955  ntrivcvgmul  15956  zprod  15991  dvdszrcl  16315  4sqlem1  17008  4sqlem19  17023  ramub1lem2  17087  structcnvcnv  17213  strleun  17217  fvsetsid  17228  smndex1sgrp  18970  gicer  19347  cntzsgrpcl  19404  symgbasfi  19449  mvdco  19515  symgsssg  19537  efglem  19786  efgtf  19792  efgtlen  19796  efginvrel2  19797  efginvrel1  19798  efgsfo  19809  efgredlemg  19812  efgredleme  19813  efgredlemd  19814  efgredlemc  19815  efgredlem  19817  efgred  19818  efgrelexlemb  19820  efgcpbllemb  19825  frgpinv  19834  frgpuplem  19842  frgpupf  19843  frgpup1  19845  frgpnabllem2  19944  gsumval3lem1  19975  gsumval3lem2  19976  gsumval3  19977  fldc  20865  fldhmsubc  20866  lbsextlem3  21262  pzriprnglem10  21609  znf1o  21670  zntoslem  21675  pjpm  21827  mhp0cl  22278  ply1bascl  22332  dmtopon  23049  ordtbas  23318  leordtval2  23338  lecldbas  23345  lmfval  23358  lmbrf  23386  cnconst2  23409  conncompcld  23560  hauspwdom  23627  txuni2  23691  xkouni  23725  xkoccn  23745  txkgen  23778  qtoptop2  23825  kqdisj  23858  hmphtop  23904  hmpher  23910  uzrest  24023  uzfbas  24024  lmflf  24131  tgpconncompeqg  24238  tgpconncomp  24239  ustn0  24347  xmeter  24559  isngp2  24723  xrtgioo  24933  iccntr  24948  xmetdcn  24965  metdcn  24967  metdscn2  24984  cnheiborlem  25082  reparphti  25125  lmmbrf  25390  iscau4  25407  iscauf  25408  caucfil  25411  lmclimf  25432  volf  25657  uniioombllem3  25713  uniioombllem4  25714  uniioombllem5  25715  volcn  25734  mbfimaopnlem  25783  mbflimsup  25794  i1f1  25818  itg2lcl  25855  itgioo  25944  itgsplitioo  25966  limcflflem  26008  limcflf  26009  limcresi  26013  lhop  26144  dvfsumlem1  26154  dvfsumlem2  26155  dvfsumlem3  26156  dvfsumlem4  26157  dvfsumrlimge0  26158  dvfsumrlim  26159  dvfsumrlim2  26160  dvfsum2  26162  vieta1lem1  26440  vieta1lem2  26441  psercnlem2  26553  psercnlem1  26554  psercn  26555  pserdvlem1  26556  pserdvlem2  26557  pserdv  26558  pserdv2  26559  logcnlem5  26777  dvlog  26782  dvlog2lem  26783  dvlog2  26784  dvcncxp1  26874  dvcnsqrt  26875  cxpcn3lem  26878  cxpcn3  26879  sqrtcn  26881  1cubr  26973  atansssdm  27064  jensen  27119  musum  27321  ppiub  27334  lgsquadlem1  27510  lgsquadlem2  27511  lgsquadlem3  27512  2sqlem7  27554  nosupbnd1lem1  27838  nosupbnd2  27846  noinfbnd1lem1  27853  cutsf  27951  leftssold  28030  rightssold  28031  mulsproplem12  28286  mulsproplem13  28287  mulsproplem14  28288  precsexlem8  28373  onssno  28413  nnssn0s  28480  dfnns2  28531  bdaypw2n0bndlem  28622  axtgcgrrflx  28697  axtgcgrid  28698  axtgsegcon  28699  axtg5seg  28700  axtgbtwnid  28701  axtgpasch  28702  axtgcont1  28703  tglng  28781  disjxwwlkn  30203  frgrwopreg2  30611  phnv  31107  htthlem  31210  hlimadd  31486  hlimcaui  31529  hhsscms  31571  occllem  31596  shjshsi  31785  3oalem4  31958  pjfi  31997  dmadjss  32180  nlelshi  32353  nlelchi  32354  hmopidmchi  32444  shatomistici  32654  difxp1ss  32809  difxp2ss  32810  fcoinver  32890  opabssi  32899  mptctf  33002  ccatws1f1o  33212  gsumpart  33324  pmtrcnel2  33351  psgnfzto1stlem  33361  cycpmrn  33404  cyc3genpm  33413  unitprodclb  33646  lsmsnorb  33648  ply1degltel  33829  ply1degleel  33830  ply1degltlss  33831  evlextv  33877  vietalem  33914  constrsscn  34075  cnre2csqima  34246  raddcn  34264  zrhcntr  34314  rrhre  34356  esumsnf  34399  sxbrsiga  34625  omssubadd  34635  carsggect  34653  sitmcl  34686  oddpwdc  34689  eulerpartlem1  34702  eulerpartlemt  34706  eulerpartgbij  34707  eulerpartlemmf  34710  eulerpartlemgh  34713  sseqf  34727  ballotlemfmpn  34830  ballotth  34873  signswch  34893  ftc2re  34930  fdvposlt  34931  fdvposle  34933  bnj1146  35124  bnj1292  35148  bnj1293  35149  bnj1145  35326  bnj1177  35339  fineqvnttrclse  35470  tz9.1regs  35480  erdszelem2  35617  kur14lem3  35633  kur14lem6  35636  kur14lem7  35637  kur14lem9  35639  cvmlift2lem12  35739  mpstssv  35964  mstapst  35972  mppspstlem  35996  mppspst  35999  mthmsta  36003  mthmpps  36007  mclsppslem  36008  txpss3v  36301  pprodss4v  36307  relsset  36311  fixssdm  36329  fixssrn  36330  limitssson  36334  funpartss  36369  colinearex  36485  fneer  36787  neibastop1  36793  neibastop2lem  36794  filnetlem2  36813  filnetlem3  36814  ttcuniun  36944  ttcuni  36947  knoppcnlem10  37014  bj-tagss  37538  bj-imdirco  37756  bj-fvsnun2  37822  bj-ablssgrp  37842  bj-ablsscmn  37844  bj-vecssmod  37847  bj-fldssdrng  37854  icoreresf  37920  icoreunrn  37927  poimirlem29  38222  poimirlem30  38223  poimirlem31  38224  poimir  38226  broucube  38227  dvasin  38277  dvacos  38278  areacirc  38286  caures  38333  bnd2lem  38364  ismtyres  38381  flddivrng  38572  xrnss3v  38954  refrelsredund2  39290  toycom  39671  dihglblem2N  41992  lcdvbase  42291  mapdunirnN  42348  aks6d1c1p1rcl  42799  redvmptabs  43045  readvrec  43047  prjspreln0  43267  prjspvs  43268  prjspeclsp  43270  0prjspnrel  43285  dffltz  43292  eldiophb  43414  monotuz  43594  pwssplit4  43742  pwfi2f1o  43749  arearect  43868  cantnfresb  43977  omabs2  43985  fvnonrel  44249  rclexi  44267  rtrclex  44269  trclexi  44272  rtrclexi  44273  clcnvlem  44275  cnvrcl0  44277  cnvtrcl0  44278  dfrtrcl5  44281  dfrcl2  44326  comptiunov2i  44358  corclrcl  44359  trclrelexplem  44363  relexpaddss  44370  cotrcltrcl  44377  corcltrcl  44391  cotrclrcl  44394  frege131d  44416  0he  44434  grumnudlem  44921  uzmptshftfval  44982  binomcxplemdvbinom  44989  binomcxplemdvsum  44991  binomcxplemnotnn0  44992  modelaxreplem2  45614  rabexgf  45670  uzct  45709  disjf1o  45835  dmmptssf  45873  mptssid  45882  uzfissfz  45968  ssuzfz  45991  uzssre2  46047  uzublem  46070  uzssz2  46096  uzsscn2  46117  sumnnodd  46272  climconstmpt  46298  fnlimfvre  46314  fnlimabslt  46319  limsupubuzlem  46352  limsupubuz  46353  limsupequzmpt2  46358  limsupmnfuzlem  46366  limsupre3uzlem  46375  liminfequzmpt2  46431  ibliooicc  46611  stoweidlem44  46684  stoweidlem50  46690  stoweidlem51  46691  stoweidlem52  46692  stoweidlem57  46697  stoweidlem59  46699  fourierdlem16  46763  fourierdlem19  46766  fourierdlem21  46768  fourierdlem22  46769  fourierdlem42  46789  fourierdlem83  46829  fouriersw  46871  salexct  46974  salexct3  46982  salgencntex  46983  salgensscntex  46984  sge0less  47032  sge0fodjrnlem  47056  sge0isum  47067  ovnlerp  47202  ovn0lem  47205  hoidmv1lelem1  47231  hoidmv1lelem3  47233  hoidmvlelem1  47235  hoidmvlelem2  47236  hoidmvlelem3  47237  hoidmvlelem4  47238  ovnhoilem1  47241  ovnhoilem2  47242  opnvonmbllem2  47273  ovolval4lem1  47289  ovolval5lem3  47294  pimdecfgtioc  47355  pimincfltioc  47356  pimdecfgtioo  47357  pimincfltioo  47358  incsmflem  47381  decsmflem  47406  smflimlem2  47412  smflimlem3  47413  smflim  47417  smfrec  47429  smfmullem4  47434  smfdiv  47437  smfsuplem1  47451  smfsuplem3  47453  smfsupxr  47456  smfliminflem  47470  cfsetssfset  47716  fcoreslem2  47724  fcores  47727  gricrel  48607  clnbgrisubgrgrim  48620  isubgr3stgrlem6  48659  isubgr3stgrlem7  48660  isubgr3stgrlem8  48661  isubgr3stgr  48663  grlimgrtrilem2  48690  grlicrel  48694  oddibas  48861  2zlidl  48928  2zrngbas  48930  2zrng0  48932  fldcALTV  49020  fldhmsubcALTV  49021  dmtposss  49573  tposres3  49578  ipolub0  49689  imaidfu  49807