Theorem eqsstri 4010

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

Syntax hints:   = wceq 1539   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948

This theorem is referenced by:  eqsstrri  4011  3sstr4i  4015  ssrab3  4062  rabssab  4065  ifssun  4523  opabss  5187  brab2a  5759  relopabiALT  5813  dmopabss  5909  rnopabss  5946  resss  5999  relres  6003  rnin  6146  rnxpss  6172  cnvcnvss  6194  resdmss  6235  resssxp  6270  dfpo2  6296  predss  6309  fnres  6675  f0  6769  nfvres  6927  fvopab4ndm  7026  ffvresb  7125  mptexgf  7224  funiunfv  7250  isoini2  7341  ovssunirn  7449  dmoprabss  7519  mpondm0  7655  elmpocl  7656  exse2  7921  fabexgOLD  7943  frxp  8133  tposssxp  8237  dftpos4  8252  wfrdmssOLD  8337  smores  8374  smores2  8376  iordsmo  8379  swoer  8758  swoord1  8759  swoord2  8760  ecss  8775  ecopovsym  8841  ecopovtrn  8842  ecopover  8843  f1setex  8879  sbthlem7  9111  imafi  9335  elfiun  9452  marypha1lem  9455  marypha2lem1  9457  hartogslem1  9564  wdomima2g  9608  inf3lem1  9650  dmttrcl  9743  rnttrcl  9744  tc2  9764  frmin  9771  frrlem16  9780  frr1  9781  tz9.12lem1  9809  rankuni  9885  rankuniss  9888  rankmapu  9900  hta  9919  r0weon  10034  infxpenlem  10035  ackbij1lem9  10249  ackbij1lem10  10250  ackbij1b  10260  sdom2en01  10324  fin23lem26  10347  fin56  10415  fin1a2lem9  10430  axdc3lem  10472  axdc3lem2  10473  axcclem  10479  imadomg  10556  iundom2g  10562  smobeth  10608  canth4  10669  gruina  10840  grur1a  10841  pinn  10900  niex  10903  ltsopi  10910  ltrelpi  10911  dmaddpi  10912  dmmulpi  10913  enqex  10944  ltrelnq  10948  nqerf  10952  nqerrel  10954  dmrecnq  10990  lterpq  10992  ltrelpr  11020  enrex  11089  ltrelsr  11090  dmaddsr  11107  dmmulsr  11108  ltrelre  11156  axaddf  11167  axmulf  11168  ltrelxr  11304  lerelxr  11306  nn0ssre  12513  nn0sscn  12514  nn0ssz  12619  uzsupss  12964  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  fz1ssfz0  13645  uzsup  13885  fzfi  13995  swrd00  14664  01sqrexlem3  15265  cau3  15376  caubnd  15379  limsupgre  15499  rlimpm  15518  rlimclim  15564  isercolllem1  15683  isercolllem2  15684  isercoll  15686  caurcvg  15695  caucvg  15697  iseraltlem2  15701  iseraltlem3  15702  zsum  15736  fsumcvg3  15747  climfsum  15838  ackbijnn  15846  divcnvshft  15873  infcvgaux1i  15875  clim2prod  15906  ntrivcvg  15915  ntrivcvgfvn0  15917  ntrivcvgtail  15918  ntrivcvgmullem  15919  ntrivcvgmul  15920  zprod  15955  dvdszrcl  16277  4sqlem1  16968  4sqlem19  16983  ramub1lem2  17047  structcnvcnv  17172  strleun  17176  fvsetsid  17187  smndex1sgrp  18890  gicer  19264  cntzsgrpcl  19321  symgbasfi  19364  mvdco  19431  symgsssg  19453  efglem  19702  efgtf  19708  efgtlen  19712  efginvrel2  19713  efginvrel1  19714  efgsfo  19725  efgredlemg  19728  efgredleme  19729  efgredlemd  19730  efgredlemc  19731  efgredlem  19733  efgred  19734  efgrelexlemb  19736  efgcpbllemb  19741  frgpinv  19750  frgpuplem  19758  frgpupf  19759  frgpup1  19761  frgpnabllem2  19860  gsumval3lem1  19891  gsumval3lem2  19892  gsumval3  19893  fldc  20753  fldhmsubc  20754  lbsextlem3  21130  pzriprnglem10  21463  znf1o  21524  zntoslem  21529  pjpm  21682  mhp0cl  22098  ply1bascl  22153  dmtopon  22877  ordtbas  23146  leordtval2  23166  lecldbas  23173  lmfval  23186  lmbrf  23214  cnconst2  23237  conncompcld  23388  hauspwdom  23455  txuni2  23519  xkouni  23553  xkoccn  23573  txkgen  23606  qtoptop2  23653  kqdisj  23686  hmphtop  23732  hmpher  23738  uzrest  23851  uzfbas  23852  lmflf  23959  tgpconncompeqg  24066  tgpconncomp  24067  ustn0  24175  xmeter  24388  isngp2  24554  xrtgioo  24764  iccntr  24779  xmetdcn  24796  metdcn  24798  metdscn2  24815  icchmeoOLD  24908  cnheiborlem  24922  reparphti  24965  lmmbrf  25232  iscau4  25249  iscauf  25250  caucfil  25253  lmclimf  25274  volf  25500  uniioombllem3  25556  uniioombllem4  25557  uniioombllem5  25558  volcn  25577  mbfimaopnlem  25626  mbflimsup  25637  i1f1  25661  itg2lcl  25698  itgioo  25787  itgsplitioo  25809  limcflflem  25851  limcflf  25852  limcresi  25856  lhop  25991  dvfsumlem1  26002  dvfsumlem2  26003  dvfsumlem2OLD  26004  dvfsumlem3  26005  dvfsumlem4  26006  dvfsumrlimge0  26007  dvfsumrlim  26008  dvfsumrlim2  26009  dvfsum2  26011  vieta1lem1  26288  vieta1lem2  26289  psercnlem2  26404  psercnlem1  26405  psercn  26406  pserdvlem1  26407  pserdvlem2  26408  pserdv  26409  pserdv2  26410  logcnlem5  26624  dvlog  26629  dvlog2lem  26630  dvlog2  26631  dvcncxp1  26721  dvcnsqrt  26722  cxpcn3lem  26726  cxpcn3  26727  sqrtcn  26729  1cubr  26821  atansssdm  26912  jensen  26968  musum  27170  ppiub  27184  lgsquadlem1  27360  lgsquadlem2  27361  lgsquadlem3  27362  2sqlem7  27404  nosupbnd1lem1  27689  nosupbnd2  27697  noinfbnd1lem1  27704  scutf  27793  leftssold  27853  rightssold  27854  mulsproplem12  28089  mulsproplem13  28090  mulsproplem14  28091  precsexlem8  28174  onssno  28213  nnssn0s  28262  dfnns2  28298  axtgcgrrflx  28406  axtgcgrid  28407  axtgsegcon  28408  axtg5seg  28409  axtgbtwnid  28410  axtgpasch  28411  axtgcont1  28412  tglng  28490  disjxwwlkn  29861  frgrwopreg2  30266  phnv  30761  htthlem  30864  hlimadd  31140  hlimcaui  31183  hhsscms  31225  occllem  31250  shjshsi  31439  3oalem4  31612  pjfi  31651  dmadjss  31834  nlelshi  32007  nlelchi  32008  hmopidmchi  32098  shatomistici  32308  difxp1ss  32469  difxp2ss  32470  fcoinver  32552  opabssi  32560  mptctf  32664  ccatws1f1o  32876  gsumpart  32999  pmtrcnel2  33049  psgnfzto1stlem  33059  cycpmrn  33102  cyc3genpm  33111  unitprodclb  33352  lsmsnorb  33354  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  constrsscn  33720  cnre2csqima  33869  raddcn  33887  zrhcntr  33939  rrhre  33981  esumsnf  34024  sxbrsiga  34251  omssubadd  34261  carsggect  34279  sitmcl  34312  oddpwdc  34315  eulerpartlem1  34328  eulerpartlemt  34332  eulerpartgbij  34333  eulerpartlemmf  34336  eulerpartlemgh  34339  sseqf  34353  ballotlemfmpn  34456  ballotth  34499  signswch  34535  ftc2re  34572  fdvposlt  34573  fdvposle  34575  bnj1146  34764  bnj1292  34788  bnj1293  34789  bnj1145  34966  bnj1177  34979  erdszelem2  35156  kur14lem3  35172  kur14lem6  35175  kur14lem7  35176  kur14lem9  35178  cvmlift2lem12  35278  mpstssv  35503  mstapst  35511  mppspstlem  35535  mppspst  35538  mthmsta  35542  mthmpps  35546  mclsppslem  35547  txpss3v  35838  pprodss4v  35844  relsset  35848  fixssdm  35866  fixssrn  35867  limitssson  35871  funpartss  35904  colinearex  36020  fneer  36313  neibastop1  36319  neibastop2lem  36320  filnetlem2  36339  filnetlem3  36340  knoppcnlem10  36462  bj-tagss  36940  bj-imdirco  37150  bj-fvsnun2  37216  bj-ablssgrp  37236  bj-ablsscmn  37238  bj-vecssmod  37241  bj-fldssdrng  37248  icoreresf  37312  icoreunrn  37319  poimirlem29  37615  poimirlem30  37616  poimirlem31  37617  poimir  37619  broucube  37620  dvasin  37670  dvacos  37671  areacirc  37679  caures  37726  bnd2lem  37757  ismtyres  37774  flddivrng  37965  xrnss3v  38332  refrelsredund2  38593  toycom  38933  dihglblem2N  41255  lcdvbase  41554  mapdunirnN  41611  aks6d1c1p1rcl  42068  redvmptabs  42353  readvrec  42355  prjspreln0  42582  prjspvs  42583  prjspeclsp  42585  0prjspnrel  42600  dffltz  42607  eldiophb  42731  monotuz  42916  pwssplit4  43064  pwfi2f1o  43071  arearect  43190  cantnfresb  43299  omabs2  43307  fvnonrel  43572  rclexi  43590  rtrclex  43592  trclexi  43595  rtrclexi  43596  clcnvlem  43598  cnvrcl0  43600  cnvtrcl0  43601  dfrtrcl5  43604  dfrcl2  43649  comptiunov2i  43681  corclrcl  43682  trclrelexplem  43686  relexpaddss  43693  cotrcltrcl  43700  corcltrcl  43714  cotrclrcl  43717  frege131d  43739  0he  43757  grumnudlem  44261  uzmptshftfval  44322  binomcxplemdvbinom  44329  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  modelaxreplem2  44953  rabexgf  44986  uzct  45025  disjf1o  45153  dmmptssf  45194  mptssid  45204  uzfissfz  45294  ssuzfz  45317  uzssre2  45375  uzublem  45398  uzssz2  45424  uzsscn2  45445  sumnnodd  45602  climconstmpt  45630  fnlimfvre  45646  fnlimabslt  45651  limsupvaluz  45680  limsupubuzlem  45684  limsupubuz  45685  limsupequzmpt2  45690  limsupmnfuzlem  45698  limsupre3uzlem  45707  liminfequzmpt2  45763  ibliooicc  45943  stoweidlem44  46016  stoweidlem50  46022  stoweidlem51  46023  stoweidlem52  46024  stoweidlem57  46029  stoweidlem59  46031  fourierdlem16  46095  fourierdlem19  46098  fourierdlem21  46100  fourierdlem22  46101  fourierdlem42  46121  fourierdlem83  46161  fouriersw  46203  salexct  46306  salexct3  46314  salgencntex  46315  salgensscntex  46316  sge0less  46364  sge0fodjrnlem  46388  sge0isum  46399  ovnlerp  46534  ovn0lem  46537  hoidmv1lelem1  46563  hoidmv1lelem3  46565  hoidmvlelem1  46567  hoidmvlelem2  46568  hoidmvlelem3  46569  hoidmvlelem4  46570  ovnhoilem1  46573  ovnhoilem2  46574  opnvonmbllem2  46605  ovolval4lem1  46621  ovolval5lem3  46626  pimdecfgtioc  46687  pimincfltioc  46688  pimdecfgtioo  46689  pimincfltioo  46690  incsmflem  46713  decsmflem  46738  smflimlem2  46744  smflimlem3  46745  smflim  46749  smfrec  46761  smfmullem4  46766  smfdiv  46769  smfsuplem1  46783  smfsuplem3  46785  smfsupxr  46788  smfliminflem  46802  cfsetssfset  47026  fcoreslem2  47034  fcores  47037  gricrel  47846  clnbgrisubgrgrim  47858  isubgr3stgrlem6  47896  isubgr3stgrlem7  47897  isubgr3stgrlem8  47898  isubgr3stgr  47900  grlimgrtrilem2  47920  grlicrel  47924  oddibas  48047  2zlidl  48114  2zrngbas  48116  2zrng0  48118  fldcALTV  48206  fldhmsubcALTV  48207  dmtposss  48735  tposres3  48740  ipolub0  48849