Theorem eqsstri 3993

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  eqsstrri  3994  3sstr4i  3998  ssrab3  4045  rabssab  4048  ifssun  4506  opabss  5171  brab2a  5732  relopabiALT  5786  dmopabss  5882  rnopabss  5919  resss  5972  relres  5976  rnin  6119  rnxpss  6145  cnvcnvss  6167  resdmss  6208  resssxp  6243  dfpo2  6269  predss  6282  fnres  6645  f0  6741  nfvres  6899  fvopab4ndm  6998  ffvresb  7097  mptexgf  7196  funiunfv  7222  isoini2  7314  ovssunirn  7423  dmoprabss  7493  mpondm0  7629  elmpocl  7630  exse2  7893  fabexgOLD  7915  frxp  8105  tposssxp  8209  dftpos4  8224  smores  8321  smores2  8323  iordsmo  8326  swoer  8702  swoord1  8703  swoord2  8704  ecss  8722  ecopovsym  8792  ecopovtrn  8793  ecopover  8794  f1setex  8830  sbthlem7  9057  imafi  9264  elfiun  9381  marypha1lem  9384  marypha2lem1  9386  hartogslem1  9495  wdomima2g  9539  inf3lem1  9581  dmttrcl  9674  rnttrcl  9675  tc2  9695  frmin  9702  frrlem16  9711  frr1  9712  tz9.12lem1  9740  rankuni  9816  rankuniss  9819  rankmapu  9831  hta  9850  r0weon  9965  infxpenlem  9966  ackbij1lem9  10180  ackbij1lem10  10181  ackbij1b  10191  sdom2en01  10255  fin23lem26  10278  fin56  10346  fin1a2lem9  10361  axdc3lem  10403  axdc3lem2  10404  axcclem  10410  imadomg  10487  iundom2g  10493  smobeth  10539  canth4  10600  gruina  10771  grur1a  10772  pinn  10831  niex  10834  ltsopi  10841  ltrelpi  10842  dmaddpi  10843  dmmulpi  10844  enqex  10875  ltrelnq  10879  nqerf  10883  nqerrel  10885  dmrecnq  10921  lterpq  10923  ltrelpr  10951  enrex  11020  ltrelsr  11021  dmaddsr  11038  dmmulsr  11039  ltrelre  11087  axaddf  11098  axmulf  11099  ltrelxr  11235  lerelxr  11237  nn0ssre  12446  nn0sscn  12447  nn0ssz  12552  uzsupss  12899  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  fz1ssfz0  13584  uzsup  13825  fzfi  13937  swrd00  14609  01sqrexlem3  15210  cau3  15322  caubnd  15325  limsupgre  15447  rlimpm  15466  rlimclim  15512  isercolllem1  15631  isercolllem2  15632  isercoll  15634  caurcvg  15643  caucvg  15645  iseraltlem2  15649  iseraltlem3  15650  zsum  15684  fsumcvg3  15695  climfsum  15786  ackbijnn  15794  divcnvshft  15821  infcvgaux1i  15823  clim2prod  15854  ntrivcvg  15863  ntrivcvgfvn0  15865  ntrivcvgtail  15866  ntrivcvgmullem  15867  ntrivcvgmul  15868  zprod  15903  dvdszrcl  16227  4sqlem1  16919  4sqlem19  16934  ramub1lem2  16998  structcnvcnv  17123  strleun  17127  fvsetsid  17138  smndex1sgrp  18835  gicer  19209  cntzsgrpcl  19266  symgbasfi  19309  mvdco  19375  symgsssg  19397  efglem  19646  efgtf  19652  efgtlen  19656  efginvrel2  19657  efginvrel1  19658  efgsfo  19669  efgredlemg  19672  efgredleme  19673  efgredlemd  19674  efgredlemc  19675  efgredlem  19677  efgred  19678  efgrelexlemb  19680  efgcpbllemb  19685  frgpinv  19694  frgpuplem  19702  frgpupf  19703  frgpup1  19705  frgpnabllem2  19804  gsumval3lem1  19835  gsumval3lem2  19836  gsumval3  19837  fldc  20693  fldhmsubc  20694  lbsextlem3  21070  pzriprnglem10  21400  znf1o  21461  zntoslem  21466  pjpm  21617  mhp0cl  22033  ply1bascl  22088  dmtopon  22810  ordtbas  23079  leordtval2  23099  lecldbas  23106  lmfval  23119  lmbrf  23147  cnconst2  23170  conncompcld  23321  hauspwdom  23388  txuni2  23452  xkouni  23486  xkoccn  23506  txkgen  23539  qtoptop2  23586  kqdisj  23619  hmphtop  23665  hmpher  23671  uzrest  23784  uzfbas  23785  lmflf  23892  tgpconncompeqg  23999  tgpconncomp  24000  ustn0  24108  xmeter  24321  isngp2  24485  xrtgioo  24695  iccntr  24710  xmetdcn  24727  metdcn  24729  metdscn2  24746  icchmeoOLD  24839  cnheiborlem  24853  reparphti  24896  lmmbrf  25162  iscau4  25179  iscauf  25180  caucfil  25183  lmclimf  25204  volf  25430  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  volcn  25507  mbfimaopnlem  25556  mbflimsup  25567  i1f1  25591  itg2lcl  25628  itgioo  25717  itgsplitioo  25739  limcflflem  25781  limcflf  25782  limcresi  25786  lhop  25921  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlimge0  25937  dvfsumrlim  25938  dvfsumrlim2  25939  dvfsum2  25941  vieta1lem1  26218  vieta1lem2  26219  psercnlem2  26334  psercnlem1  26335  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  pserdv  26339  pserdv2  26340  logcnlem5  26555  dvlog  26560  dvlog2lem  26561  dvlog2  26562  dvcncxp1  26652  dvcnsqrt  26653  cxpcn3lem  26657  cxpcn3  26658  sqrtcn  26660  1cubr  26752  atansssdm  26843  jensen  26899  musum  27101  ppiub  27115  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  2sqlem7  27335  nosupbnd1lem1  27620  nosupbnd2  27628  noinfbnd1lem1  27635  scutf  27724  leftssold  27790  rightssold  27791  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  precsexlem8  28116  onssno  28155  nnssn0s  28214  dfnns2  28261  axtgcgrrflx  28389  axtgcgrid  28390  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgcont1  28395  tglng  28473  disjxwwlkn  29843  frgrwopreg2  30248  phnv  30743  htthlem  30846  hlimadd  31122  hlimcaui  31165  hhsscms  31207  occllem  31232  shjshsi  31421  3oalem4  31594  pjfi  31633  dmadjss  31816  nlelshi  31989  nlelchi  31990  hmopidmchi  32080  shatomistici  32290  difxp1ss  32451  difxp2ss  32452  fcoinver  32533  opabssi  32541  mptctf  32641  ccatws1f1o  32873  gsumpart  32997  pmtrcnel2  33047  psgnfzto1stlem  33057  cycpmrn  33100  cyc3genpm  33109  unitprodclb  33360  lsmsnorb  33362  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  constrsscn  33730  cnre2csqima  33901  raddcn  33919  zrhcntr  33969  rrhre  34011  esumsnf  34054  sxbrsiga  34281  omssubadd  34291  carsggect  34309  sitmcl  34342  oddpwdc  34345  eulerpartlem1  34358  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemmf  34366  eulerpartlemgh  34369  sseqf  34383  ballotlemfmpn  34486  ballotth  34529  signswch  34552  ftc2re  34589  fdvposlt  34590  fdvposle  34592  bnj1146  34781  bnj1292  34805  bnj1293  34806  bnj1145  34983  bnj1177  34996  erdszelem2  35179  kur14lem3  35195  kur14lem6  35198  kur14lem7  35199  kur14lem9  35201  cvmlift2lem12  35301  mpstssv  35526  mstapst  35534  mppspstlem  35558  mppspst  35561  mthmsta  35565  mthmpps  35569  mclsppslem  35570  txpss3v  35866  pprodss4v  35872  relsset  35876  fixssdm  35894  fixssrn  35895  limitssson  35899  funpartss  35932  colinearex  36048  fneer  36341  neibastop1  36347  neibastop2lem  36348  filnetlem2  36367  filnetlem3  36368  knoppcnlem10  36490  bj-tagss  36968  bj-imdirco  37178  bj-fvsnun2  37244  bj-ablssgrp  37264  bj-ablsscmn  37266  bj-vecssmod  37269  bj-fldssdrng  37276  icoreresf  37340  icoreunrn  37347  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimir  37647  broucube  37648  dvasin  37698  dvacos  37699  areacirc  37707  caures  37754  bnd2lem  37785  ismtyres  37802  flddivrng  37993  xrnss3v  38354  refrelsredund2  38624  toycom  38966  dihglblem2N  41288  lcdvbase  41587  mapdunirnN  41644  aks6d1c1p1rcl  42096  redvmptabs  42348  readvrec  42350  prjspreln0  42597  prjspvs  42598  prjspeclsp  42600  0prjspnrel  42615  dffltz  42622  eldiophb  42745  monotuz  42930  pwssplit4  43078  pwfi2f1o  43085  arearect  43204  cantnfresb  43313  omabs2  43321  fvnonrel  43586  rclexi  43604  rtrclex  43606  trclexi  43609  rtrclexi  43610  clcnvlem  43612  cnvrcl0  43614  cnvtrcl0  43615  dfrtrcl5  43618  dfrcl2  43663  comptiunov2i  43695  corclrcl  43696  trclrelexplem  43700  relexpaddss  43707  cotrcltrcl  43714  corcltrcl  43728  cotrclrcl  43731  frege131d  43753  0he  43771  grumnudlem  44274  uzmptshftfval  44335  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  modelaxreplem2  44969  rabexgf  45018  uzct  45057  disjf1o  45185  dmmptssf  45226  mptssid  45235  uzfissfz  45322  ssuzfz  45345  uzssre2  45403  uzublem  45426  uzssz2  45452  uzsscn2  45473  sumnnodd  45628  climconstmpt  45656  fnlimfvre  45672  fnlimabslt  45677  limsupvaluz  45706  limsupubuzlem  45710  limsupubuz  45711  limsupequzmpt2  45716  limsupmnfuzlem  45724  limsupre3uzlem  45733  liminfequzmpt2  45789  ibliooicc  45969  stoweidlem44  46042  stoweidlem50  46048  stoweidlem51  46049  stoweidlem52  46050  stoweidlem57  46055  stoweidlem59  46057  fourierdlem16  46121  fourierdlem19  46124  fourierdlem21  46126  fourierdlem22  46127  fourierdlem42  46147  fourierdlem83  46187  fouriersw  46229  salexct  46332  salexct3  46340  salgencntex  46341  salgensscntex  46342  sge0less  46390  sge0fodjrnlem  46414  sge0isum  46425  ovnlerp  46560  ovn0lem  46563  hoidmv1lelem1  46589  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  ovnhoilem1  46599  ovnhoilem2  46600  opnvonmbllem2  46631  ovolval4lem1  46647  ovolval5lem3  46652  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  incsmflem  46739  decsmflem  46764  smflimlem2  46770  smflimlem3  46771  smflim  46775  smfrec  46787  smfmullem4  46792  smfdiv  46795  smfsuplem1  46809  smfsuplem3  46811  smfsupxr  46814  smfliminflem  46828  cfsetssfset  47057  fcoreslem2  47065  fcores  47068  gricrel  47919  clnbgrisubgrgrim  47932  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  isubgr3stgrlem8  47972  isubgr3stgr  47974  grlimgrtrilem2  47994  grlicrel  47998  oddibas  48161  2zlidl  48228  2zrngbas  48230  2zrng0  48232  fldcALTV  48320  fldhmsubcALTV  48321  dmtposss  48864  tposres3  48869  ipolub0  48980  imaidfu  49099