Theorem eqsstri 3963

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

Syntax hints:   = wceq 1542   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-ss 3902

This theorem is referenced by:  eqsstrri  3964  3sstr4i  3968  ssrab3  4015  rabssab  4018  ifssun  4474  opabss  5138  brab2a  5713  relopabiALT  5768  dmopabss  5862  rnopabss  5899  resss  5955  relres  5959  rnin  6099  rnxpss  6125  cnvcnvss  6147  resdmss  6188  resssxp  6223  dfpo2  6249  predss  6262  fnres  6614  f0  6710  nfvres  6867  fvopab4ndm  6967  ffvresb  7067  mptexgf  7166  funiunfv  7192  isoini2  7283  ovssunirn  7392  dmoprabss  7460  mpondm0  7596  elmpocl  7597  exse2  7857  fabexgOLD  7879  frxp  8065  tposssxp  8169  dftpos4  8184  smores  8281  smores2  8283  iordsmo  8286  swoer  8664  swoord1  8665  swoord2  8666  ecss  8684  ecopovsym  8755  ecopovtrn  8756  ecopover  8757  f1setex  8793  sbthlem7  9020  imafi  9214  elfiun  9332  marypha1lem  9335  marypha2lem1  9337  hartogslem1  9446  wdomima2g  9490  inf3lem1  9538  dmttrcl  9631  rnttrcl  9632  tc2  9650  frmin  9662  frrlem16  9671  frr1  9672  tz9.12lem1  9700  rankuni  9776  rankuniss  9779  rankmapu  9791  hta  9810  r0weon  9923  infxpenlem  9924  ackbij1lem9  10138  ackbij1lem10  10139  ackbij1b  10149  sdom2en01  10213  fin23lem26  10236  fin56  10304  fin1a2lem9  10319  axdc3lem  10361  axdc3lem2  10362  axcclem  10368  imadomg  10445  iundom2g  10451  smobeth  10498  canth4  10559  gruina  10730  grur1a  10731  pinn  10790  niex  10793  ltsopi  10800  ltrelpi  10801  dmaddpi  10802  dmmulpi  10803  enqex  10834  ltrelnq  10838  nqerf  10842  nqerrel  10844  dmrecnq  10880  lterpq  10882  ltrelpr  10910  enrex  10979  ltrelsr  10980  dmaddsr  10997  dmmulsr  10998  ltrelre  11046  axaddf  11057  axmulf  11058  ltrelxr  11195  lerelxr  11197  nn0ssre  12430  nn0sscn  12431  nn0ssz  12536  uzsupss  12879  rpnnen1lem1  12917  rpnnen1lem3  12918  rpnnen1lem5  12920  fz1ssfz0  13566  uzsup  13811  fzfi  13923  swrd00  14596  01sqrexlem3  15195  cau3  15307  caubnd  15310  limsupgre  15432  rlimpm  15451  rlimclim  15497  isercolllem1  15616  isercolllem2  15617  isercoll  15619  caurcvg  15628  caucvg  15630  iseraltlem2  15634  iseraltlem3  15635  zsum  15669  fsumcvg3  15680  climfsum  15772  ackbijnn  15782  divcnvshft  15809  infcvgaux1i  15811  clim2prod  15842  ntrivcvg  15851  ntrivcvgfvn0  15853  ntrivcvgtail  15854  ntrivcvgmullem  15855  ntrivcvgmul  15856  zprod  15891  dvdszrcl  16215  4sqlem1  16908  4sqlem19  16923  ramub1lem2  16987  structcnvcnv  17112  strleun  17116  fvsetsid  17127  smndex1sgrp  18868  gicer  19241  cntzsgrpcl  19298  symgbasfi  19343  mvdco  19409  symgsssg  19431  efglem  19680  efgtf  19686  efgtlen  19690  efginvrel2  19691  efginvrel1  19692  efgsfo  19703  efgredlemg  19706  efgredleme  19707  efgredlemd  19708  efgredlemc  19709  efgredlem  19711  efgred  19712  efgrelexlemb  19714  efgcpbllemb  19719  frgpinv  19728  frgpuplem  19736  frgpupf  19737  frgpup1  19739  frgpnabllem2  19838  gsumval3lem1  19869  gsumval3lem2  19870  gsumval3  19871  fldc  20750  fldhmsubc  20751  lbsextlem3  21147  pzriprnglem10  21459  znf1o  21520  zntoslem  21525  pjpm  21677  mhp0cl  22101  ply1bascl  22155  dmtopon  22876  ordtbas  23145  leordtval2  23165  lecldbas  23172  lmfval  23185  lmbrf  23213  cnconst2  23236  conncompcld  23387  hauspwdom  23454  txuni2  23518  xkouni  23552  xkoccn  23572  txkgen  23605  qtoptop2  23652  kqdisj  23685  hmphtop  23731  hmpher  23737  uzrest  23850  uzfbas  23851  lmflf  23958  tgpconncompeqg  24065  tgpconncomp  24066  ustn0  24174  xmeter  24386  isngp2  24550  xrtgioo  24760  iccntr  24775  xmetdcn  24792  metdcn  24794  metdscn2  24811  cnheiborlem  24909  reparphti  24952  lmmbrf  25217  iscau4  25234  iscauf  25235  caucfil  25238  lmclimf  25259  volf  25484  uniioombllem3  25540  uniioombllem4  25541  uniioombllem5  25542  volcn  25561  mbfimaopnlem  25610  mbflimsup  25621  i1f1  25645  itg2lcl  25682  itgioo  25771  itgsplitioo  25793  limcflflem  25835  limcflf  25836  limcresi  25840  lhop  25971  dvfsumlem1  25981  dvfsumlem2  25982  dvfsumlem3  25983  dvfsumlem4  25984  dvfsumrlimge0  25985  dvfsumrlim  25986  dvfsumrlim2  25987  dvfsum2  25989  vieta1lem1  26264  vieta1lem2  26265  psercnlem2  26377  psercnlem1  26378  psercn  26379  pserdvlem1  26380  pserdvlem2  26381  pserdv  26382  pserdv2  26383  logcnlem5  26598  dvlog  26603  dvlog2lem  26604  dvlog2  26605  dvcncxp1  26695  dvcnsqrt  26696  cxpcn3lem  26699  cxpcn3  26700  sqrtcn  26702  1cubr  26794  atansssdm  26885  jensen  26940  musum  27142  ppiub  27155  lgsquadlem1  27331  lgsquadlem2  27332  lgsquadlem3  27333  2sqlem7  27375  nosupbnd1lem1  27660  nosupbnd2  27668  noinfbnd1lem1  27675  cutsf  27772  leftssold  27851  rightssold  27852  mulsproplem12  28107  mulsproplem13  28108  mulsproplem14  28109  precsexlem8  28194  onssno  28234  nnssn0s  28301  dfnns2  28352  bdaypw2n0bndlem  28443  axtgcgrrflx  28518  axtgcgrid  28519  axtgsegcon  28520  axtg5seg  28521  axtgbtwnid  28522  axtgpasch  28523  axtgcont1  28524  tglng  28602  disjxwwlkn  29969  frgrwopreg2  30377  phnv  30873  htthlem  30976  hlimadd  31252  hlimcaui  31295  hhsscms  31337  occllem  31362  shjshsi  31551  3oalem4  31724  pjfi  31763  dmadjss  31946  nlelshi  32119  nlelchi  32120  hmopidmchi  32210  shatomistici  32420  difxp1ss  32580  difxp2ss  32581  fcoinver  32662  opabssi  32674  mptctf  32777  ccatws1f1o  32999  gsumpart  33112  pmtrcnel2  33139  psgnfzto1stlem  33149  cycpmrn  33192  cyc3genpm  33201  unitprodclb  33437  lsmsnorb  33439  ply1degltel  33642  ply1degleel  33643  ply1degltlss  33644  evlextv  33674  vietalem  33711  constrsscn  33872  cnre2csqima  34043  raddcn  34061  zrhcntr  34111  rrhre  34153  esumsnf  34196  sxbrsiga  34422  omssubadd  34432  carsggect  34450  sitmcl  34483  oddpwdc  34486  eulerpartlem1  34499  eulerpartlemt  34503  eulerpartgbij  34504  eulerpartlemmf  34507  eulerpartlemgh  34510  sseqf  34524  ballotlemfmpn  34627  ballotth  34670  signswch  34693  ftc2re  34730  fdvposlt  34731  fdvposle  34733  bnj1146  34921  bnj1292  34945  bnj1293  34946  bnj1145  35123  bnj1177  35136  fineqvnttrclse  35256  tz9.1regs  35266  erdszelem2  35362  kur14lem3  35378  kur14lem6  35381  kur14lem7  35382  kur14lem9  35384  cvmlift2lem12  35484  mpstssv  35709  mstapst  35717  mppspstlem  35741  mppspst  35744  mthmsta  35748  mthmpps  35752  mclsppslem  35753  txpss3v  36046  pprodss4v  36052  relsset  36056  fixssdm  36074  fixssrn  36075  limitssson  36079  funpartss  36114  colinearex  36230  fneer  36523  neibastop1  36529  neibastop2lem  36530  filnetlem2  36549  filnetlem3  36550  ttcuniun  36680  ttcuni  36683  knoppcnlem10  36750  bj-tagss  37275  bj-imdirco  37492  bj-fvsnun2  37558  bj-ablssgrp  37578  bj-ablsscmn  37580  bj-vecssmod  37583  bj-fldssdrng  37590  icoreresf  37656  icoreunrn  37663  poimirlem29  37958  poimirlem30  37959  poimirlem31  37960  poimir  37962  broucube  37963  dvasin  38013  dvacos  38014  areacirc  38022  caures  38069  bnd2lem  38100  ismtyres  38117  flddivrng  38308  xrnss3v  38690  refrelsredund2  39026  toycom  39407  dihglblem2N  41728  lcdvbase  42027  mapdunirnN  42084  aks6d1c1p1rcl  42535  redvmptabs  42780  readvrec  42782  prjspreln0  43030  prjspvs  43031  prjspeclsp  43033  0prjspnrel  43048  dffltz  43055  eldiophb  43177  monotuz  43357  pwssplit4  43505  pwfi2f1o  43512  arearect  43631  cantnfresb  43740  omabs2  43748  fvnonrel  44012  rclexi  44030  rtrclex  44032  trclexi  44035  rtrclexi  44036  clcnvlem  44038  cnvrcl0  44040  cnvtrcl0  44041  dfrtrcl5  44044  dfrcl2  44089  comptiunov2i  44121  corclrcl  44122  trclrelexplem  44126  relexpaddss  44133  cotrcltrcl  44140  corcltrcl  44154  cotrclrcl  44157  frege131d  44179  0he  44197  grumnudlem  44700  uzmptshftfval  44761  binomcxplemdvbinom  44768  binomcxplemdvsum  44770  binomcxplemnotnn0  44771  modelaxreplem2  45394  rabexgf  45443  uzct  45482  disjf1o  45609  dmmptssf  45649  mptssid  45658  uzfissfz  45744  ssuzfz  45767  uzssre2  45823  uzublem  45846  uzssz2  45872  uzsscn2  45893  sumnnodd  46048  climconstmpt  46074  fnlimfvre  46090  fnlimabslt  46095  limsupvaluz  46124  limsupubuzlem  46128  limsupubuz  46129  limsupequzmpt2  46134  limsupmnfuzlem  46142  limsupre3uzlem  46151  liminfequzmpt2  46207  ibliooicc  46387  stoweidlem44  46460  stoweidlem50  46466  stoweidlem51  46467  stoweidlem52  46468  stoweidlem57  46473  stoweidlem59  46475  fourierdlem16  46539  fourierdlem19  46542  fourierdlem21  46544  fourierdlem22  46545  fourierdlem42  46565  fourierdlem83  46605  fouriersw  46647  salexct  46750  salexct3  46758  salgencntex  46759  salgensscntex  46760  sge0less  46808  sge0fodjrnlem  46832  sge0isum  46843  ovnlerp  46978  ovn0lem  46981  hoidmv1lelem1  47007  hoidmv1lelem3  47009  hoidmvlelem1  47011  hoidmvlelem2  47012  hoidmvlelem3  47013  hoidmvlelem4  47014  ovnhoilem1  47017  ovnhoilem2  47018  opnvonmbllem2  47049  ovolval4lem1  47065  ovolval5lem3  47070  pimdecfgtioc  47131  pimincfltioc  47132  pimdecfgtioo  47133  pimincfltioo  47134  incsmflem  47157  decsmflem  47182  smflimlem2  47188  smflimlem3  47189  smflim  47193  smfrec  47205  smfmullem4  47210  smfdiv  47213  smfsuplem1  47227  smfsuplem3  47229  smfsupxr  47232  smfliminflem  47246  cfsetssfset  47492  fcoreslem2  47500  fcores  47503  gricrel  48383  clnbgrisubgrgrim  48396  isubgr3stgrlem6  48435  isubgr3stgrlem7  48436  isubgr3stgrlem8  48437  isubgr3stgr  48439  grlimgrtrilem2  48466  grlicrel  48470  oddibas  48637  2zlidl  48704  2zrngbas  48706  2zrng0  48708  fldcALTV  48796  fldhmsubcALTV  48797  dmtposss  49339  tposres3  49344  ipolub0  49455  imaidfu  49573