Theorem eqsstri 4011

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

Syntax hints:   = wceq 1533   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961

This theorem is referenced by:  eqsstrri  4012  ssrab2OLD  4074  ssrab3  4076  rabssab  4079  ifssun  4547  opabss  5213  brab2a  5771  relopabiALT  5825  dmopabss  5921  resss  6007  relres  6011  rnin  6153  rnxpss  6178  cnvcnvss  6200  resdmss  6241  resssxp  6276  dfpo2  6302  predss  6315  fnres  6683  f0  6778  nfvres  6937  fvopab4ndm  7034  ffvresb  7134  mptexgf  7234  funiunfv  7258  isoini2  7346  ovssunirn  7455  dmoprabss  7523  mpondm0  7661  elmpocl  7662  exse2  7925  fabexg  7943  frxp  8131  tposssxp  8236  dftpos4  8251  wfrdmssOLD  8336  smores  8373  smores2  8375  iordsmo  8378  swoer  8755  swoord1  8756  swoord2  8757  ecss  8772  ecopovsym  8838  ecopovtrn  8839  ecopover  8840  f1setex  8876  sbthlem7  9114  nnfiOLD  9257  imafiALT  9371  elfiun  9455  marypha1lem  9458  marypha2lem1  9460  hartogslem1  9567  wdomima2g  9611  inf3lem1  9653  dmttrcl  9746  rnttrcl  9747  tc2  9767  frmin  9774  frrlem16  9783  frr1  9784  tz9.12lem1  9812  rankuni  9888  rankuniss  9891  rankmapu  9903  hta  9922  r0weon  10037  infxpenlem  10038  ackbij1lem9  10253  ackbij1lem10  10254  ackbij1b  10264  sdom2en01  10327  fin23lem26  10350  fin56  10418  fin1a2lem9  10433  axdc3lem  10475  axdc3lem2  10476  axcclem  10482  imadomg  10559  iundom2g  10565  smobeth  10611  canth4  10672  gruina  10843  grur1a  10844  pinn  10903  niex  10906  ltsopi  10913  ltrelpi  10914  dmaddpi  10915  dmmulpi  10916  enqex  10947  ltrelnq  10951  nqerf  10955  nqerrel  10957  dmrecnq  10993  lterpq  10995  ltrelpr  11023  enrex  11092  ltrelsr  11093  dmaddsr  11110  dmmulsr  11111  ltrelre  11159  axaddf  11170  axmulf  11171  ltrelxr  11307  lerelxr  11309  nn0ssre  12509  nn0sscn  12510  nn0ssz  12614  uzsupss  12957  rpnnen1lem1  12995  rpnnen1lem3  12996  rpnnen1lem5  12998  fz1ssfz0  13632  uzsup  13864  fzfi  13973  swrd00  14630  01sqrexlem3  15227  cau3  15338  caubnd  15341  limsupgre  15461  rlimpm  15480  rlimclim  15526  isercolllem1  15647  isercolllem2  15648  isercoll  15650  caurcvg  15659  caucvg  15661  iseraltlem2  15665  iseraltlem3  15666  zsum  15700  fsumcvg3  15711  climfsum  15802  ackbijnn  15810  divcnvshft  15837  infcvgaux1i  15839  clim2prod  15870  ntrivcvg  15879  ntrivcvgfvn0  15881  ntrivcvgtail  15882  ntrivcvgmullem  15883  ntrivcvgmul  15884  zprod  15917  dvdszrcl  16239  4sqlem1  16920  4sqlem19  16935  ramub1lem2  16999  structcnvcnv  17125  strleun  17129  fvsetsid  17140  smndex1sgrp  18868  gicer  19240  cntzsgrpcl  19297  symgbasfi  19345  mvdco  19412  symgsssg  19434  efglem  19683  efgtf  19689  efgtlen  19693  efginvrel2  19694  efginvrel1  19695  efgsfo  19706  efgredlemg  19709  efgredleme  19710  efgredlemd  19711  efgredlemc  19712  efgredlem  19714  efgred  19715  efgrelexlemb  19717  efgcpbllemb  19722  frgpinv  19731  frgpuplem  19739  frgpupf  19740  frgpup1  19742  frgpnabllem2  19841  gsumval3lem1  19872  gsumval3lem2  19873  gsumval3  19874  fldc  20684  fldhmsubc  20685  lbsextlem3  21060  pzriprnglem10  21433  znf1o  21502  zntoslem  21507  pjpm  21659  mhp0cl  22093  ply1bascl  22146  dmtopon  22869  ordtbas  23140  leordtval2  23160  lecldbas  23167  lmfval  23180  lmbrf  23208  cnconst2  23231  conncompcld  23382  hauspwdom  23449  txuni2  23513  xkouni  23547  xkoccn  23567  txkgen  23600  qtoptop2  23647  kqdisj  23680  hmphtop  23726  hmpher  23732  uzrest  23845  uzfbas  23846  lmflf  23953  tgpconncompeqg  24060  tgpconncomp  24061  ustn0  24169  xmeter  24383  isngp2  24550  xrtgioo  24766  iccntr  24781  xmetdcn  24798  metdcn  24800  metdscn2  24817  icchmeoOLD  24910  cnheiborlem  24924  reparphti  24967  lmmbrf  25234  iscau4  25251  iscauf  25252  caucfil  25255  lmclimf  25276  volf  25502  uniioombllem3  25558  uniioombllem4  25559  uniioombllem5  25560  volcn  25579  mbfimaopnlem  25628  mbflimsup  25639  i1f1  25663  itg2lcl  25701  itgioo  25789  itgsplitioo  25811  limcflflem  25853  limcflf  25854  limcresi  25858  lhop  25993  dvfsumlem1  26004  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumlem3  26007  dvfsumlem4  26008  dvfsumrlimge0  26009  dvfsumrlim  26010  dvfsumrlim2  26011  dvfsum2  26013  vieta1lem1  26290  vieta1lem2  26291  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  pserdv  26411  pserdv2  26412  logcnlem5  26625  dvlog  26630  dvlog2lem  26631  dvlog2  26632  dvcncxp1  26722  dvcnsqrt  26723  cxpcn3lem  26727  cxpcn3  26728  sqrtcn  26730  1cubr  26819  atansssdm  26910  jensen  26966  musum  27168  ppiub  27182  lgsquadlem1  27358  lgsquadlem2  27359  lgsquadlem3  27360  2sqlem7  27402  nosupbnd1lem1  27687  nosupbnd2  27695  noinfbnd1lem1  27702  scutf  27791  leftssold  27851  rightssold  27852  mulsproplem12  28077  mulsproplem13  28078  mulsproplem14  28079  precsexlem8  28162  onssno  28197  nnssn0s  28243  axtgcgrrflx  28338  axtgcgrid  28339  axtgsegcon  28340  axtg5seg  28341  axtgbtwnid  28342  axtgpasch  28343  axtgcont1  28344  tglng  28422  disjxwwlkn  29796  frgrwopreg2  30201  phnv  30696  htthlem  30799  hlimadd  31075  hlimcaui  31118  hhsscms  31160  occllem  31185  shjshsi  31374  3oalem4  31547  pjfi  31586  dmadjss  31769  nlelshi  31942  nlelchi  31943  hmopidmchi  32033  shatomistici  32243  difxp1ss  32398  difxp2ss  32399  fcoinver  32473  opabssi  32482  mptctf  32581  ccatws1f1o  32761  gsumpart  32859  pmtrcnel2  32903  psgnfzto1stlem  32913  cycpmrn  32956  cyc3genpm  32965  unitprodclb  33201  lsmsnorb  33203  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  cnre2csqima  33643  raddcn  33661  rrhre  33753  esumsnf  33814  sxbrsiga  34041  omssubadd  34051  carsggect  34069  sitmcl  34102  oddpwdc  34105  eulerpartlem1  34118  eulerpartlemt  34122  eulerpartgbij  34123  eulerpartlemmf  34126  eulerpartlemgh  34129  sseqf  34143  ballotlemfmpn  34245  ballotth  34288  signswch  34324  ftc2re  34361  fdvposlt  34362  fdvposle  34364  bnj1146  34553  bnj1292  34577  bnj1293  34578  bnj1145  34755  bnj1177  34768  erdszelem2  34933  kur14lem3  34949  kur14lem6  34952  kur14lem7  34953  kur14lem9  34955  cvmlift2lem12  35055  mpstssv  35280  mstapst  35288  mppspstlem  35312  mppspst  35315  mthmsta  35319  mthmpps  35323  mclsppslem  35324  txpss3v  35605  pprodss4v  35611  relsset  35615  fixssdm  35633  fixssrn  35634  limitssson  35638  funpartss  35671  colinearex  35787  fneer  35968  neibastop1  35974  neibastop2lem  35975  filnetlem2  35994  filnetlem3  35995  knoppcnlem10  36108  bj-tagss  36590  bj-imdirco  36800  bj-fvsnun2  36866  bj-ablssgrp  36886  bj-ablsscmn  36888  bj-vecssmod  36891  bj-fldssdrng  36898  icoreresf  36962  icoreunrn  36969  poimirlem29  37253  poimirlem30  37254  poimirlem31  37255  poimir  37257  broucube  37258  dvasin  37308  dvacos  37309  areacirc  37317  caures  37364  bnd2lem  37395  ismtyres  37412  flddivrng  37603  xrnss3v  37974  refrelsredund2  38235  toycom  38575  dihglblem2N  40897  lcdvbase  41196  mapdunirnN  41253  aks6d1c1p1rcl  41711  prjspreln0  42168  prjspvs  42169  prjspeclsp  42171  0prjspnrel  42186  dffltz  42193  eldiophb  42319  monotuz  42504  pwssplit4  42655  pwfi2f1o  42662  arearect  42785  cantnfresb  42895  omabs2  42903  fvnonrel  43169  rclexi  43187  rtrclex  43189  trclexi  43192  rtrclexi  43193  clcnvlem  43195  cnvrcl0  43197  cnvtrcl0  43198  dfrtrcl5  43201  dfrcl2  43246  comptiunov2i  43278  corclrcl  43279  trclrelexplem  43283  relexpaddss  43290  cotrcltrcl  43297  corcltrcl  43311  cotrclrcl  43314  frege131d  43336  0he  43354  grumnudlem  43864  uzmptshftfval  43925  binomcxplemdvbinom  43932  binomcxplemdvsum  43934  binomcxplemnotnn0  43935  rabexgf  44528  uzct  44569  disjf1o  44703  dmmptssf  44744  mptssid  44754  uzfissfz  44846  ssuzfz  44869  uzssre2  44927  uzublem  44950  uzssz2  44976  uzsscn2  44998  sumnnodd  45156  climconstmpt  45184  fnlimfvre  45200  fnlimabslt  45205  limsupvaluz  45234  limsupubuzlem  45238  limsupubuz  45239  limsupequzmpt2  45244  limsupmnfuzlem  45252  limsupre3uzlem  45261  liminfequzmpt2  45317  ibliooicc  45497  stoweidlem44  45570  stoweidlem50  45576  stoweidlem51  45577  stoweidlem52  45578  stoweidlem57  45583  stoweidlem59  45585  fourierdlem16  45649  fourierdlem19  45652  fourierdlem21  45654  fourierdlem22  45655  fourierdlem42  45675  fourierdlem83  45715  fouriersw  45757  salexct  45860  salexct3  45868  salgencntex  45869  salgensscntex  45870  sge0less  45918  sge0fodjrnlem  45942  sge0isum  45953  ovnlerp  46088  ovn0lem  46091  hoidmv1lelem1  46117  hoidmv1lelem3  46119  hoidmvlelem1  46121  hoidmvlelem2  46122  hoidmvlelem3  46123  hoidmvlelem4  46124  ovnhoilem1  46127  ovnhoilem2  46128  opnvonmbllem2  46159  ovolval4lem1  46175  ovolval5lem3  46180  pimdecfgtioc  46241  pimincfltioc  46242  pimdecfgtioo  46243  pimincfltioo  46244  incsmflem  46267  decsmflem  46292  smflimlem2  46298  smflimlem3  46299  smflim  46303  smfrec  46315  smfmullem4  46320  smfdiv  46323  smfsuplem1  46337  smfsuplem3  46339  smfsupxr  46342  smfliminflem  46356  cfsetssfset  46576  fcoreslem2  46584  fcores  46587  gricrel  47371  oddibas  47421  2zlidl  47488  2zrngbas  47490  2zrng0  47492  fldcALTV  47580  fldhmsubcALTV  47581  ipolub0  48189