Theorem eqsstri 3976

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

Syntax hints:   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  eqsstrri  3977  3sstr4i  3981  ssrab3  4027  rabssab  4030  ifssun  4488  opabss  5150  brab2a  5704  relopabiALT  5758  dmopabss  5853  rnopabss  5890  resss  5945  relres  5949  rnin  6088  rnxpss  6114  cnvcnvss  6136  resdmss  6177  resssxp  6212  dfpo2  6238  predss  6251  fnres  6603  f0  6699  nfvres  6855  fvopab4ndm  6954  ffvresb  7053  mptexgf  7151  funiunfv  7177  isoini2  7268  ovssunirn  7377  dmoprabss  7445  mpondm0  7581  elmpocl  7582  exse2  7842  fabexgOLD  7864  frxp  8051  tposssxp  8155  dftpos4  8170  smores  8267  smores2  8269  iordsmo  8272  swoer  8648  swoord1  8649  swoord2  8650  ecss  8668  ecopovsym  8738  ecopovtrn  8739  ecopover  8740  f1setex  8776  sbthlem7  9001  imafi  9194  elfiun  9309  marypha1lem  9312  marypha2lem1  9314  hartogslem1  9423  wdomima2g  9467  inf3lem1  9513  dmttrcl  9606  rnttrcl  9607  tc2  9625  frmin  9637  frrlem16  9646  frr1  9647  tz9.12lem1  9675  rankuni  9751  rankuniss  9754  rankmapu  9766  hta  9785  r0weon  9898  infxpenlem  9899  ackbij1lem9  10113  ackbij1lem10  10114  ackbij1b  10124  sdom2en01  10188  fin23lem26  10211  fin56  10279  fin1a2lem9  10294  axdc3lem  10336  axdc3lem2  10337  axcclem  10343  imadomg  10420  iundom2g  10426  smobeth  10472  canth4  10533  gruina  10704  grur1a  10705  pinn  10764  niex  10767  ltsopi  10774  ltrelpi  10775  dmaddpi  10776  dmmulpi  10777  enqex  10808  ltrelnq  10812  nqerf  10816  nqerrel  10818  dmrecnq  10854  lterpq  10856  ltrelpr  10884  enrex  10953  ltrelsr  10954  dmaddsr  10971  dmmulsr  10972  ltrelre  11020  axaddf  11031  axmulf  11032  ltrelxr  11168  lerelxr  11170  nn0ssre  12380  nn0sscn  12381  nn0ssz  12486  uzsupss  12833  rpnnen1lem1  12871  rpnnen1lem3  12872  rpnnen1lem5  12874  fz1ssfz0  13518  uzsup  13762  fzfi  13874  swrd00  14547  01sqrexlem3  15146  cau3  15258  caubnd  15261  limsupgre  15383  rlimpm  15402  rlimclim  15448  isercolllem1  15567  isercolllem2  15568  isercoll  15570  caurcvg  15579  caucvg  15581  iseraltlem2  15585  iseraltlem3  15586  zsum  15620  fsumcvg3  15631  climfsum  15722  ackbijnn  15730  divcnvshft  15757  infcvgaux1i  15759  clim2prod  15790  ntrivcvg  15799  ntrivcvgfvn0  15801  ntrivcvgtail  15802  ntrivcvgmullem  15803  ntrivcvgmul  15804  zprod  15839  dvdszrcl  16163  4sqlem1  16855  4sqlem19  16870  ramub1lem2  16934  structcnvcnv  17059  strleun  17063  fvsetsid  17074  smndex1sgrp  18811  gicer  19184  cntzsgrpcl  19241  symgbasfi  19286  mvdco  19352  symgsssg  19374  efglem  19623  efgtf  19629  efgtlen  19633  efginvrel2  19634  efginvrel1  19635  efgsfo  19646  efgredlemg  19649  efgredleme  19650  efgredlemd  19651  efgredlemc  19652  efgredlem  19654  efgred  19655  efgrelexlemb  19657  efgcpbllemb  19662  frgpinv  19671  frgpuplem  19679  frgpupf  19680  frgpup1  19682  frgpnabllem2  19781  gsumval3lem1  19812  gsumval3lem2  19813  gsumval3  19814  fldc  20694  fldhmsubc  20695  lbsextlem3  21092  pzriprnglem10  21422  znf1o  21483  zntoslem  21488  pjpm  21640  mhp0cl  22056  ply1bascl  22111  dmtopon  22833  ordtbas  23102  leordtval2  23122  lecldbas  23129  lmfval  23142  lmbrf  23170  cnconst2  23193  conncompcld  23344  hauspwdom  23411  txuni2  23475  xkouni  23509  xkoccn  23529  txkgen  23562  qtoptop2  23609  kqdisj  23642  hmphtop  23688  hmpher  23694  uzrest  23807  uzfbas  23808  lmflf  23915  tgpconncompeqg  24022  tgpconncomp  24023  ustn0  24131  xmeter  24343  isngp2  24507  xrtgioo  24717  iccntr  24732  xmetdcn  24749  metdcn  24751  metdscn2  24768  icchmeoOLD  24861  cnheiborlem  24875  reparphti  24918  lmmbrf  25184  iscau4  25201  iscauf  25202  caucfil  25205  lmclimf  25226  volf  25452  uniioombllem3  25508  uniioombllem4  25509  uniioombllem5  25510  volcn  25529  mbfimaopnlem  25578  mbflimsup  25589  i1f1  25613  itg2lcl  25650  itgioo  25739  itgsplitioo  25761  limcflflem  25803  limcflf  25804  limcresi  25808  lhop  25943  dvfsumlem1  25954  dvfsumlem2  25955  dvfsumlem2OLD  25956  dvfsumlem3  25957  dvfsumlem4  25958  dvfsumrlimge0  25959  dvfsumrlim  25960  dvfsumrlim2  25961  dvfsum2  25963  vieta1lem1  26240  vieta1lem2  26241  psercnlem2  26356  psercnlem1  26357  psercn  26358  pserdvlem1  26359  pserdvlem2  26360  pserdv  26361  pserdv2  26362  logcnlem5  26577  dvlog  26582  dvlog2lem  26583  dvlog2  26584  dvcncxp1  26674  dvcnsqrt  26675  cxpcn3lem  26679  cxpcn3  26680  sqrtcn  26682  1cubr  26774  atansssdm  26865  jensen  26921  musum  27123  ppiub  27137  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  2sqlem7  27357  nosupbnd1lem1  27642  nosupbnd2  27650  noinfbnd1lem1  27657  scutf  27748  leftssold  27819  rightssold  27820  mulsproplem12  28061  mulsproplem13  28062  mulsproplem14  28063  precsexlem8  28147  onssno  28186  nnssn0s  28245  dfnns2  28292  axtgcgrrflx  28435  axtgcgrid  28436  axtgsegcon  28437  axtg5seg  28438  axtgbtwnid  28439  axtgpasch  28440  axtgcont1  28441  tglng  28519  disjxwwlkn  29886  frgrwopreg2  30291  phnv  30786  htthlem  30889  hlimadd  31165  hlimcaui  31208  hhsscms  31250  occllem  31275  shjshsi  31464  3oalem4  31637  pjfi  31676  dmadjss  31859  nlelshi  32032  nlelchi  32033  hmopidmchi  32123  shatomistici  32333  difxp1ss  32494  difxp2ss  32495  fcoinver  32576  opabssi  32588  mptctf  32691  ccatws1f1o  32924  gsumpart  33029  pmtrcnel2  33051  psgnfzto1stlem  33061  cycpmrn  33104  cyc3genpm  33113  unitprodclb  33346  lsmsnorb  33348  ply1degltel  33547  ply1degleel  33548  ply1degltlss  33549  constrsscn  33745  cnre2csqima  33916  raddcn  33934  zrhcntr  33984  rrhre  34026  esumsnf  34069  sxbrsiga  34295  omssubadd  34305  carsggect  34323  sitmcl  34356  oddpwdc  34359  eulerpartlem1  34372  eulerpartlemt  34376  eulerpartgbij  34377  eulerpartlemmf  34380  eulerpartlemgh  34383  sseqf  34397  ballotlemfmpn  34500  ballotth  34543  signswch  34566  ftc2re  34603  fdvposlt  34604  fdvposle  34606  bnj1146  34795  bnj1292  34819  bnj1293  34820  bnj1145  34997  bnj1177  35010  tz9.1regs  35122  fineqvnttrclse  35136  erdszelem2  35228  kur14lem3  35244  kur14lem6  35247  kur14lem7  35248  kur14lem9  35250  cvmlift2lem12  35350  mpstssv  35575  mstapst  35583  mppspstlem  35607  mppspst  35610  mthmsta  35614  mthmpps  35618  mclsppslem  35619  txpss3v  35912  pprodss4v  35918  relsset  35922  fixssdm  35940  fixssrn  35941  limitssson  35945  funpartss  35978  colinearex  36094  fneer  36387  neibastop1  36393  neibastop2lem  36394  filnetlem2  36413  filnetlem3  36414  knoppcnlem10  36536  bj-tagss  37014  bj-imdirco  37224  bj-fvsnun2  37290  bj-ablssgrp  37310  bj-ablsscmn  37312  bj-vecssmod  37315  bj-fldssdrng  37322  icoreresf  37386  icoreunrn  37393  poimirlem29  37689  poimirlem30  37690  poimirlem31  37691  poimir  37693  broucube  37694  dvasin  37744  dvacos  37745  areacirc  37753  caures  37800  bnd2lem  37831  ismtyres  37848  flddivrng  38039  xrnss3v  38400  refrelsredund2  38670  toycom  39012  dihglblem2N  41333  lcdvbase  41632  mapdunirnN  41689  aks6d1c1p1rcl  42141  redvmptabs  42393  readvrec  42395  prjspreln0  42642  prjspvs  42643  prjspeclsp  42645  0prjspnrel  42660  dffltz  42667  eldiophb  42790  monotuz  42974  pwssplit4  43122  pwfi2f1o  43129  arearect  43248  cantnfresb  43357  omabs2  43365  fvnonrel  43630  rclexi  43648  rtrclex  43650  trclexi  43653  rtrclexi  43654  clcnvlem  43656  cnvrcl0  43658  cnvtrcl0  43659  dfrtrcl5  43662  dfrcl2  43707  comptiunov2i  43739  corclrcl  43740  trclrelexplem  43744  relexpaddss  43751  cotrcltrcl  43758  corcltrcl  43772  cotrclrcl  43775  frege131d  43797  0he  43815  grumnudlem  44318  uzmptshftfval  44379  binomcxplemdvbinom  44386  binomcxplemdvsum  44388  binomcxplemnotnn0  44389  modelaxreplem2  45012  rabexgf  45061  uzct  45100  disjf1o  45228  dmmptssf  45269  mptssid  45278  uzfissfz  45365  ssuzfz  45388  uzssre2  45445  uzublem  45468  uzssz2  45494  uzsscn2  45515  sumnnodd  45670  climconstmpt  45696  fnlimfvre  45712  fnlimabslt  45717  limsupvaluz  45746  limsupubuzlem  45750  limsupubuz  45751  limsupequzmpt2  45756  limsupmnfuzlem  45764  limsupre3uzlem  45773  liminfequzmpt2  45829  ibliooicc  46009  stoweidlem44  46082  stoweidlem50  46088  stoweidlem51  46089  stoweidlem52  46090  stoweidlem57  46095  stoweidlem59  46097  fourierdlem16  46161  fourierdlem19  46164  fourierdlem21  46166  fourierdlem22  46167  fourierdlem42  46187  fourierdlem83  46227  fouriersw  46269  salexct  46372  salexct3  46380  salgencntex  46381  salgensscntex  46382  sge0less  46430  sge0fodjrnlem  46454  sge0isum  46465  ovnlerp  46600  ovn0lem  46603  hoidmv1lelem1  46629  hoidmv1lelem3  46631  hoidmvlelem1  46633  hoidmvlelem2  46634  hoidmvlelem3  46635  hoidmvlelem4  46636  ovnhoilem1  46639  ovnhoilem2  46640  opnvonmbllem2  46671  ovolval4lem1  46687  ovolval5lem3  46692  pimdecfgtioc  46753  pimincfltioc  46754  pimdecfgtioo  46755  pimincfltioo  46756  incsmflem  46779  decsmflem  46804  smflimlem2  46810  smflimlem3  46811  smflim  46815  smfrec  46827  smfmullem4  46832  smfdiv  46835  smfsuplem1  46849  smfsuplem3  46851  smfsupxr  46854  smfliminflem  46868  cfsetssfset  47087  fcoreslem2  47095  fcores  47098  gricrel  47950  clnbgrisubgrgrim  47963  isubgr3stgrlem6  48002  isubgr3stgrlem7  48003  isubgr3stgrlem8  48004  isubgr3stgr  48006  grlimgrtrilem2  48033  grlicrel  48037  oddibas  48204  2zlidl  48271  2zrngbas  48273  2zrng0  48275  fldcALTV  48363  fldhmsubcALTV  48364  dmtposss  48907  tposres3  48912  ipolub0  49023  imaidfu  49142