Theorem eqsstri 4029

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

Syntax hints:   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  eqsstrri  4030  ssrab3  4091  rabssab  4094  ifssun  4547  opabss  5211  brab2a  5781  relopabiALT  5835  dmopabss  5931  rnopabss  5968  resss  6021  relres  6025  rnin  6168  rnxpss  6193  cnvcnvss  6215  resdmss  6256  resssxp  6291  dfpo2  6317  predss  6330  fnres  6695  f0  6789  nfvres  6947  fvopab4ndm  7045  ffvresb  7144  mptexgf  7241  funiunfv  7267  isoini2  7358  ovssunirn  7466  dmoprabss  7535  mpondm0  7672  elmpocl  7673  exse2  7939  fabexgOLD  7959  frxp  8149  tposssxp  8253  dftpos4  8268  wfrdmssOLD  8353  smores  8390  smores2  8392  iordsmo  8395  swoer  8774  swoord1  8775  swoord2  8776  ecss  8791  ecopovsym  8857  ecopovtrn  8858  ecopover  8859  f1setex  8895  sbthlem7  9127  imafi  9350  elfiun  9467  marypha1lem  9470  marypha2lem1  9472  hartogslem1  9579  wdomima2g  9623  inf3lem1  9665  dmttrcl  9758  rnttrcl  9759  tc2  9779  frmin  9786  frrlem16  9795  frr1  9796  tz9.12lem1  9824  rankuni  9900  rankuniss  9903  rankmapu  9915  hta  9934  r0weon  10049  infxpenlem  10050  ackbij1lem9  10264  ackbij1lem10  10265  ackbij1b  10275  sdom2en01  10339  fin23lem26  10362  fin56  10430  fin1a2lem9  10445  axdc3lem  10487  axdc3lem2  10488  axcclem  10494  imadomg  10571  iundom2g  10577  smobeth  10623  canth4  10684  gruina  10855  grur1a  10856  pinn  10915  niex  10918  ltsopi  10925  ltrelpi  10926  dmaddpi  10927  dmmulpi  10928  enqex  10959  ltrelnq  10963  nqerf  10967  nqerrel  10969  dmrecnq  11005  lterpq  11007  ltrelpr  11035  enrex  11104  ltrelsr  11105  dmaddsr  11122  dmmulsr  11123  ltrelre  11171  axaddf  11182  axmulf  11183  ltrelxr  11319  lerelxr  11321  nn0ssre  12527  nn0sscn  12528  nn0ssz  12633  uzsupss  12979  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  fz1ssfz0  13659  uzsup  13899  fzfi  14009  swrd00  14678  01sqrexlem3  15279  cau3  15390  caubnd  15393  limsupgre  15513  rlimpm  15532  rlimclim  15578  isercolllem1  15697  isercolllem2  15698  isercoll  15700  caurcvg  15709  caucvg  15711  iseraltlem2  15715  iseraltlem3  15716  zsum  15750  fsumcvg3  15761  climfsum  15852  ackbijnn  15860  divcnvshft  15887  infcvgaux1i  15889  clim2prod  15920  ntrivcvg  15929  ntrivcvgfvn0  15931  ntrivcvgtail  15932  ntrivcvgmullem  15933  ntrivcvgmul  15934  zprod  15969  dvdszrcl  16291  4sqlem1  16981  4sqlem19  16996  ramub1lem2  17060  structcnvcnv  17186  strleun  17190  fvsetsid  17201  smndex1sgrp  18933  gicer  19307  cntzsgrpcl  19364  symgbasfi  19410  mvdco  19477  symgsssg  19499  efglem  19748  efgtf  19754  efgtlen  19758  efginvrel2  19759  efginvrel1  19760  efgsfo  19771  efgredlemg  19774  efgredleme  19775  efgredlemd  19776  efgredlemc  19777  efgredlem  19779  efgred  19780  efgrelexlemb  19782  efgcpbllemb  19787  frgpinv  19796  frgpuplem  19804  frgpupf  19805  frgpup1  19807  frgpnabllem2  19906  gsumval3lem1  19937  gsumval3lem2  19938  gsumval3  19939  fldc  20801  fldhmsubc  20802  lbsextlem3  21179  pzriprnglem10  21518  znf1o  21587  zntoslem  21592  pjpm  21745  mhp0cl  22167  ply1bascl  22220  dmtopon  22944  ordtbas  23215  leordtval2  23235  lecldbas  23242  lmfval  23255  lmbrf  23283  cnconst2  23306  conncompcld  23457  hauspwdom  23524  txuni2  23588  xkouni  23622  xkoccn  23642  txkgen  23675  qtoptop2  23722  kqdisj  23755  hmphtop  23801  hmpher  23807  uzrest  23920  uzfbas  23921  lmflf  24028  tgpconncompeqg  24135  tgpconncomp  24136  ustn0  24244  xmeter  24458  isngp2  24625  xrtgioo  24841  iccntr  24856  xmetdcn  24873  metdcn  24875  metdscn2  24892  icchmeoOLD  24985  cnheiborlem  24999  reparphti  25042  lmmbrf  25309  iscau4  25326  iscauf  25327  caucfil  25330  lmclimf  25351  volf  25577  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  volcn  25654  mbfimaopnlem  25703  mbflimsup  25714  i1f1  25738  itg2lcl  25776  itgioo  25865  itgsplitioo  25887  limcflflem  25929  limcflf  25930  limcresi  25934  lhop  26069  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlimge0  26085  dvfsumrlim  26086  dvfsumrlim2  26087  dvfsum2  26089  vieta1lem1  26366  vieta1lem2  26367  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  pserdv  26487  pserdv2  26488  logcnlem5  26702  dvlog  26707  dvlog2lem  26708  dvlog2  26709  dvcncxp1  26799  dvcnsqrt  26800  cxpcn3lem  26804  cxpcn3  26805  sqrtcn  26807  1cubr  26899  atansssdm  26990  jensen  27046  musum  27248  ppiub  27262  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  2sqlem7  27482  nosupbnd1lem1  27767  nosupbnd2  27775  noinfbnd1lem1  27782  scutf  27871  leftssold  27931  rightssold  27932  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  precsexlem8  28252  onssno  28291  nnssn0s  28340  dfnns2  28376  axtgcgrrflx  28484  axtgcgrid  28485  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgcont1  28490  tglng  28568  disjxwwlkn  29942  frgrwopreg2  30347  phnv  30842  htthlem  30945  hlimadd  31221  hlimcaui  31264  hhsscms  31306  occllem  31331  shjshsi  31520  3oalem4  31693  pjfi  31732  dmadjss  31915  nlelshi  32088  nlelchi  32089  hmopidmchi  32179  shatomistici  32389  difxp1ss  32549  difxp2ss  32550  fcoinver  32623  opabssi  32632  mptctf  32734  ccatws1f1o  32920  gsumpart  33042  pmtrcnel2  33092  psgnfzto1stlem  33102  cycpmrn  33145  cyc3genpm  33154  unitprodclb  33396  lsmsnorb  33398  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  constrsscn  33744  cnre2csqima  33871  raddcn  33889  zrhcntr  33941  rrhre  33983  esumsnf  34044  sxbrsiga  34271  omssubadd  34281  carsggect  34299  sitmcl  34332  oddpwdc  34335  eulerpartlem1  34348  eulerpartlemt  34352  eulerpartgbij  34353  eulerpartlemmf  34356  eulerpartlemgh  34359  sseqf  34373  ballotlemfmpn  34475  ballotth  34518  signswch  34554  ftc2re  34591  fdvposlt  34592  fdvposle  34594  bnj1146  34783  bnj1292  34807  bnj1293  34808  bnj1145  34985  bnj1177  34998  erdszelem2  35176  kur14lem3  35192  kur14lem6  35195  kur14lem7  35196  kur14lem9  35198  cvmlift2lem12  35298  mpstssv  35523  mstapst  35531  mppspstlem  35555  mppspst  35558  mthmsta  35562  mthmpps  35566  mclsppslem  35567  txpss3v  35859  pprodss4v  35865  relsset  35869  fixssdm  35887  fixssrn  35888  limitssson  35892  funpartss  35925  colinearex  36041  fneer  36335  neibastop1  36341  neibastop2lem  36342  filnetlem2  36361  filnetlem3  36362  knoppcnlem10  36484  bj-tagss  36962  bj-imdirco  37172  bj-fvsnun2  37238  bj-ablssgrp  37258  bj-ablsscmn  37260  bj-vecssmod  37263  bj-fldssdrng  37270  icoreresf  37334  icoreunrn  37341  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimir  37639  broucube  37640  dvasin  37690  dvacos  37691  areacirc  37699  caures  37746  bnd2lem  37777  ismtyres  37794  flddivrng  37985  xrnss3v  38353  refrelsredund2  38614  toycom  38954  dihglblem2N  41276  lcdvbase  41575  mapdunirnN  41632  aks6d1c1p1rcl  42089  redvmptabs  42368  readvrec  42370  prjspreln0  42595  prjspvs  42596  prjspeclsp  42598  0prjspnrel  42613  dffltz  42620  eldiophb  42744  monotuz  42929  pwssplit4  43077  pwfi2f1o  43084  arearect  43203  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  44280  uzmptshftfval  44341  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  modelaxreplem2  44943  rabexgf  44961  uzct  45002  disjf1o  45133  dmmptssf  45174  mptssid  45184  uzfissfz  45275  ssuzfz  45298  uzssre2  45356  uzublem  45379  uzssz2  45405  uzsscn2  45427  sumnnodd  45585  climconstmpt  45613  fnlimfvre  45629  fnlimabslt  45634  limsupvaluz  45663  limsupubuzlem  45667  limsupubuz  45668  limsupequzmpt2  45673  limsupmnfuzlem  45681  limsupre3uzlem  45690  liminfequzmpt2  45746  ibliooicc  45926  stoweidlem44  45999  stoweidlem50  46005  stoweidlem51  46006  stoweidlem52  46007  stoweidlem57  46012  stoweidlem59  46014  fourierdlem16  46078  fourierdlem19  46081  fourierdlem21  46083  fourierdlem22  46084  fourierdlem42  46104  fourierdlem83  46144  fouriersw  46186  salexct  46289  salexct3  46297  salgencntex  46298  salgensscntex  46299  sge0less  46347  sge0fodjrnlem  46371  sge0isum  46382  ovnlerp  46517  ovn0lem  46520  hoidmv1lelem1  46546  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  ovnhoilem1  46556  ovnhoilem2  46557  opnvonmbllem2  46588  ovolval4lem1  46604  ovolval5lem3  46609  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  incsmflem  46696  decsmflem  46721  smflimlem2  46727  smflimlem3  46728  smflim  46732  smfrec  46744  smfmullem4  46749  smfdiv  46752  smfsuplem1  46766  smfsuplem3  46768  smfsupxr  46771  smfliminflem  46785  cfsetssfset  47005  fcoreslem2  47013  fcores  47016  gricrel  47825  clnbgrisubgrgrim  47837  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  isubgr3stgrlem8  47875  isubgr3stgr  47877  grlimgrtrilem2  47897  grlicrel  47901  oddibas  48016  2zlidl  48083  2zrngbas  48085  2zrng0  48087  fldcALTV  48175  fldhmsubcALTV  48176  ipolub0  48780