Theorem eqsstri 3982

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

Syntax hints:   = wceq 1540   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920

This theorem is referenced by:  eqsstrri  3983  3sstr4i  3987  ssrab3  4033  rabssab  4036  ifssun  4494  opabss  5156  brab2a  5712  relopabiALT  5766  dmopabss  5861  rnopabss  5897  resss  5952  relres  5956  rnin  6095  rnxpss  6121  cnvcnvss  6143  resdmss  6184  resssxp  6218  dfpo2  6244  predss  6257  fnres  6609  f0  6705  nfvres  6861  fvopab4ndm  6960  ffvresb  7059  mptexgf  7158  funiunfv  7184  isoini2  7276  ovssunirn  7385  dmoprabss  7453  mpondm0  7589  elmpocl  7590  exse2  7850  fabexgOLD  7872  frxp  8059  tposssxp  8163  dftpos4  8178  smores  8275  smores2  8277  iordsmo  8280  swoer  8656  swoord1  8657  swoord2  8658  ecss  8676  ecopovsym  8746  ecopovtrn  8747  ecopover  8748  f1setex  8784  sbthlem7  9010  imafi  9204  elfiun  9320  marypha1lem  9323  marypha2lem1  9325  hartogslem1  9434  wdomima2g  9478  inf3lem1  9524  dmttrcl  9617  rnttrcl  9618  tc2  9638  frmin  9645  frrlem16  9654  frr1  9655  tz9.12lem1  9683  rankuni  9759  rankuniss  9762  rankmapu  9774  hta  9793  r0weon  9906  infxpenlem  9907  ackbij1lem9  10121  ackbij1lem10  10122  ackbij1b  10132  sdom2en01  10196  fin23lem26  10219  fin56  10287  fin1a2lem9  10302  axdc3lem  10344  axdc3lem2  10345  axcclem  10351  imadomg  10428  iundom2g  10434  smobeth  10480  canth4  10541  gruina  10712  grur1a  10713  pinn  10772  niex  10775  ltsopi  10782  ltrelpi  10783  dmaddpi  10784  dmmulpi  10785  enqex  10816  ltrelnq  10820  nqerf  10824  nqerrel  10826  dmrecnq  10862  lterpq  10864  ltrelpr  10892  enrex  10961  ltrelsr  10962  dmaddsr  10979  dmmulsr  10980  ltrelre  11028  axaddf  11039  axmulf  11040  ltrelxr  11176  lerelxr  11178  nn0ssre  12388  nn0sscn  12389  nn0ssz  12494  uzsupss  12841  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem5  12882  fz1ssfz0  13526  uzsup  13767  fzfi  13879  swrd00  14551  01sqrexlem3  15151  cau3  15263  caubnd  15266  limsupgre  15388  rlimpm  15407  rlimclim  15453  isercolllem1  15572  isercolllem2  15573  isercoll  15575  caurcvg  15584  caucvg  15586  iseraltlem2  15590  iseraltlem3  15591  zsum  15625  fsumcvg3  15636  climfsum  15727  ackbijnn  15735  divcnvshft  15762  infcvgaux1i  15764  clim2prod  15795  ntrivcvg  15804  ntrivcvgfvn0  15806  ntrivcvgtail  15807  ntrivcvgmullem  15808  ntrivcvgmul  15809  zprod  15844  dvdszrcl  16168  4sqlem1  16860  4sqlem19  16875  ramub1lem2  16939  structcnvcnv  17064  strleun  17068  fvsetsid  17079  smndex1sgrp  18782  gicer  19156  cntzsgrpcl  19213  symgbasfi  19258  mvdco  19324  symgsssg  19346  efglem  19595  efgtf  19601  efgtlen  19605  efginvrel2  19606  efginvrel1  19607  efgsfo  19618  efgredlemg  19621  efgredleme  19622  efgredlemd  19623  efgredlemc  19624  efgredlem  19626  efgred  19627  efgrelexlemb  19629  efgcpbllemb  19634  frgpinv  19643  frgpuplem  19651  frgpupf  19652  frgpup1  19654  frgpnabllem2  19753  gsumval3lem1  19784  gsumval3lem2  19785  gsumval3  19786  fldc  20669  fldhmsubc  20670  lbsextlem3  21067  pzriprnglem10  21397  znf1o  21458  zntoslem  21463  pjpm  21615  mhp0cl  22031  ply1bascl  22086  dmtopon  22808  ordtbas  23077  leordtval2  23097  lecldbas  23104  lmfval  23117  lmbrf  23145  cnconst2  23168  conncompcld  23319  hauspwdom  23386  txuni2  23450  xkouni  23484  xkoccn  23504  txkgen  23537  qtoptop2  23584  kqdisj  23617  hmphtop  23663  hmpher  23669  uzrest  23782  uzfbas  23783  lmflf  23890  tgpconncompeqg  23997  tgpconncomp  23998  ustn0  24106  xmeter  24319  isngp2  24483  xrtgioo  24693  iccntr  24708  xmetdcn  24725  metdcn  24727  metdscn2  24744  icchmeoOLD  24837  cnheiborlem  24851  reparphti  24894  lmmbrf  25160  iscau4  25177  iscauf  25178  caucfil  25181  lmclimf  25202  volf  25428  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  volcn  25505  mbfimaopnlem  25554  mbflimsup  25565  i1f1  25589  itg2lcl  25626  itgioo  25715  itgsplitioo  25737  limcflflem  25779  limcflf  25780  limcresi  25784  lhop  25919  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsumrlimge0  25935  dvfsumrlim  25936  dvfsumrlim2  25937  dvfsum2  25939  vieta1lem1  26216  vieta1lem2  26217  psercnlem2  26332  psercnlem1  26333  psercn  26334  pserdvlem1  26335  pserdvlem2  26336  pserdv  26337  pserdv2  26338  logcnlem5  26553  dvlog  26558  dvlog2lem  26559  dvlog2  26560  dvcncxp1  26650  dvcnsqrt  26651  cxpcn3lem  26655  cxpcn3  26656  sqrtcn  26658  1cubr  26750  atansssdm  26841  jensen  26897  musum  27099  ppiub  27113  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  2sqlem7  27333  nosupbnd1lem1  27618  nosupbnd2  27626  noinfbnd1lem1  27633  scutf  27723  leftssold  27793  rightssold  27794  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  precsexlem8  28121  onssno  28160  nnssn0s  28219  dfnns2  28266  axtgcgrrflx  28407  axtgcgrid  28408  axtgsegcon  28409  axtg5seg  28410  axtgbtwnid  28411  axtgpasch  28412  axtgcont1  28413  tglng  28491  disjxwwlkn  29858  frgrwopreg2  30263  phnv  30758  htthlem  30861  hlimadd  31137  hlimcaui  31180  hhsscms  31222  occllem  31247  shjshsi  31436  3oalem4  31609  pjfi  31648  dmadjss  31831  nlelshi  32004  nlelchi  32005  hmopidmchi  32095  shatomistici  32305  difxp1ss  32466  difxp2ss  32467  fcoinver  32548  opabssi  32558  mptctf  32660  ccatws1f1o  32893  gsumpart  33010  pmtrcnel2  33032  psgnfzto1stlem  33042  cycpmrn  33085  cyc3genpm  33094  unitprodclb  33326  lsmsnorb  33328  ply1degltel  33527  ply1degleel  33528  ply1degltlss  33529  constrsscn  33707  cnre2csqima  33878  raddcn  33896  zrhcntr  33946  rrhre  33988  esumsnf  34031  sxbrsiga  34258  omssubadd  34268  carsggect  34286  sitmcl  34319  oddpwdc  34322  eulerpartlem1  34335  eulerpartlemt  34339  eulerpartgbij  34340  eulerpartlemmf  34343  eulerpartlemgh  34346  sseqf  34360  ballotlemfmpn  34463  ballotth  34506  signswch  34529  ftc2re  34566  fdvposlt  34567  fdvposle  34569  bnj1146  34758  bnj1292  34782  bnj1293  34783  bnj1145  34960  bnj1177  34973  tz9.1regs  35067  erdszelem2  35165  kur14lem3  35181  kur14lem6  35184  kur14lem7  35185  kur14lem9  35187  cvmlift2lem12  35287  mpstssv  35512  mstapst  35520  mppspstlem  35544  mppspst  35547  mthmsta  35551  mthmpps  35555  mclsppslem  35556  txpss3v  35852  pprodss4v  35858  relsset  35862  fixssdm  35880  fixssrn  35881  limitssson  35885  funpartss  35918  colinearex  36034  fneer  36327  neibastop1  36333  neibastop2lem  36334  filnetlem2  36353  filnetlem3  36354  knoppcnlem10  36476  bj-tagss  36954  bj-imdirco  37164  bj-fvsnun2  37230  bj-ablssgrp  37250  bj-ablsscmn  37252  bj-vecssmod  37255  bj-fldssdrng  37262  icoreresf  37326  icoreunrn  37333  poimirlem29  37629  poimirlem30  37630  poimirlem31  37631  poimir  37633  broucube  37634  dvasin  37684  dvacos  37685  areacirc  37693  caures  37740  bnd2lem  37771  ismtyres  37788  flddivrng  37979  xrnss3v  38340  refrelsredund2  38610  toycom  38952  dihglblem2N  41273  lcdvbase  41572  mapdunirnN  41629  aks6d1c1p1rcl  42081  redvmptabs  42333  readvrec  42335  prjspreln0  42582  prjspvs  42583  prjspeclsp  42585  0prjspnrel  42600  dffltz  42607  eldiophb  42730  monotuz  42914  pwssplit4  43062  pwfi2f1o  43069  arearect  43188  cantnfresb  43297  omabs2  43305  fvnonrel  43570  rclexi  43588  rtrclex  43590  trclexi  43593  rtrclexi  43594  clcnvlem  43596  cnvrcl0  43598  cnvtrcl0  43599  dfrtrcl5  43602  dfrcl2  43647  comptiunov2i  43679  corclrcl  43680  trclrelexplem  43684  relexpaddss  43691  cotrcltrcl  43698  corcltrcl  43712  cotrclrcl  43715  frege131d  43737  0he  43755  grumnudlem  44258  uzmptshftfval  44319  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  modelaxreplem2  44953  rabexgf  45002  uzct  45041  disjf1o  45169  dmmptssf  45210  mptssid  45219  uzfissfz  45306  ssuzfz  45329  uzssre2  45386  uzublem  45409  uzssz2  45435  uzsscn2  45456  sumnnodd  45611  climconstmpt  45639  fnlimfvre  45655  fnlimabslt  45660  limsupvaluz  45689  limsupubuzlem  45693  limsupubuz  45694  limsupequzmpt2  45699  limsupmnfuzlem  45707  limsupre3uzlem  45716  liminfequzmpt2  45772  ibliooicc  45952  stoweidlem44  46025  stoweidlem50  46031  stoweidlem51  46032  stoweidlem52  46033  stoweidlem57  46038  stoweidlem59  46040  fourierdlem16  46104  fourierdlem19  46107  fourierdlem21  46109  fourierdlem22  46110  fourierdlem42  46130  fourierdlem83  46170  fouriersw  46212  salexct  46315  salexct3  46323  salgencntex  46324  salgensscntex  46325  sge0less  46373  sge0fodjrnlem  46397  sge0isum  46408  ovnlerp  46543  ovn0lem  46546  hoidmv1lelem1  46572  hoidmv1lelem3  46574  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  ovnhoilem1  46582  ovnhoilem2  46583  opnvonmbllem2  46614  ovolval4lem1  46630  ovolval5lem3  46635  pimdecfgtioc  46696  pimincfltioc  46697  pimdecfgtioo  46698  pimincfltioo  46699  incsmflem  46722  decsmflem  46747  smflimlem2  46753  smflimlem3  46754  smflim  46758  smfrec  46770  smfmullem4  46775  smfdiv  46778  smfsuplem1  46792  smfsuplem3  46794  smfsupxr  46797  smfliminflem  46811  cfsetssfset  47040  fcoreslem2  47048  fcores  47051  gricrel  47903  clnbgrisubgrgrim  47916  isubgr3stgrlem6  47955  isubgr3stgrlem7  47956  isubgr3stgrlem8  47957  isubgr3stgr  47959  grlimgrtrilem2  47986  grlicrel  47990  oddibas  48157  2zlidl  48224  2zrngbas  48226  2zrng0  48228  fldcALTV  48316  fldhmsubcALTV  48317  dmtposss  48860  tposres3  48865  ipolub0  48976  imaidfu  49095