Theorem eqsstri 3959

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ss 3901

This theorem is used by:  eqsstrri  3960  3sstr4i  3964  ssrab3  4010  rabssab  4013  ifssun  4503  opabss  5172  brab2a  5749  relopabiALT  5806  dmopabss  5905  rnopabss  5942  resss  5997  relresOLD  6002  rninOLD  6144  rnxpss  6170  cnvcnvss  6192  cnvcnvssOLD  6193  resdmss  6243  resssxp  6279  dfpo2  6306  predss  6319  fnres  6677  f0  6774  nfvres  6934  fvopab4ndm  7035  ffvresb  7137  mptexgf  7238  funiunfv  7262  isoini2  7357  ovssunirn  7466  dmoprabss  7534  mpondm0  7671  elmpocl  7672  exse2  7939  frxp  8151  tposssxp  8261  dftpos4  8276  smores2  8376  iordsmo  8379  swoer  8763  swoord1  8764  swoord2  8765  ecss  8783  ecopovsym  8854  ecopovtrn  8855  ecopover  8856  f1setex  8893  sbthlem7  9126  imafi  9321  elfiun  9435  marypha1lem  9438  marypha2lem1  9440  hartogslem1  9549  wdomima2g  9593  inf3lem1  9642  dmttrcl  9735  rnttrcl  9736  tc2  9754  frmin  9766  frrlem16  9775  frr1  9776  tz9.12lem1  9807  rankuni  9892  rankuniss  9896  rankmapu  9908  hta  9975  htaOLD  9976  r0weon  10104  infxpenlem  10105  ackbij1lem9  10318  ackbij1lem10  10319  ackbij1b  10329  sdom2en01  10393  fin23lem26  10416  fin56  10484  fin1a2lem9  10499  axdc3lem  10541  axdc3lem2  10542  axcclem  10548  imadomg  10626  iundom2g  10637  smobeth  10684  canth4  10745  gruina  10916  grur1a  10917  pinn  10976  niex  10979  ltsopi  10986  ltrelpi  10987  dmaddpi  10988  dmmulpi  10989  enqex  11020  ltrelnq  11024  nqerf  11028  nqerrel  11030  dmrecnq  11066  lterpq  11068  ltrelpr  11096  enrex  11165  ltrelsr  11166  dmaddsr  11183  dmmulsr  11184  ltrelre  11232  axaddf  11243  axmulf  11244  ltrelxr  11383  lerelxr  11385  nn0ssre  12623  nn0sscn  12624  nn0ssz  12729  uzsupss  13080  rpnnen1lem1  13119  rpnnen1lem3  13120  rpnnen1lem5  13122  fz1ssfz0  13770  uzsup  14016  fzfi  14128  swrd00  14806  01sqrexlem3  15426  cau3  15538  caubnd  15541  limsupgre  15663  rlimpm  15682  rlimclim  15728  isercolllem1  15847  isercolllem2  15848  isercoll  15850  caurcvg  15859  caucvg  15861  iseraltlem2  15865  iseraltlem3  15866  zsum  15899  fsumcvg3  15910  climfsum  16002  ackbijnn  16012  divcnvshft  16039  infcvgaux1i  16041  clim2prod  16072  ntrivcvg  16081  ntrivcvgfvn0  16083  ntrivcvgtail  16084  ntrivcvgmullem  16085  ntrivcvgmul  16086  zprod  16119  dvdszrcl  16442  4sqlem1  17141  4sqlem19  17156  ramub1lem2  17220  structcnvcnv  17346  strleun  17350  fvsetsid  17361  idressidex0  18875  smndex1sgrp  19122  gicer  19506  cntzsgrpcl  19563  symgbasfi  19608  mvdco  19674  symgsssg  19696  efglem  19945  efgtf  19951  efgtlen  19955  efginvrel2  19956  efginvrel1  19957  efgsfo  19968  efgredlemg  19971  efgredleme  19972  efgredlemd  19973  efgredlemc  19974  efgredlem  19976  efgred  19977  efgrelexlemb  19979  efgcpbllemb  19984  frgpinv  19993  frgpuplem  20001  frgpupf  20002  frgpup1  20004  frgpnabllem2  20103  gsumval3lem1  20134  gsumval3lem2  20135  gsumval3  20136  ricrel  20759  fldc  21056  fldhmsubc  21057  lbsextlem3  21453  pzriprnglem10  21811  znf1o  21872  zntoslem  21877  pjpm  22029  mhp0cl  22482  ply1bascl  22536  dmtopon  23256  ordtbas  23525  leordtval2  23545  lecldbas  23552  lmfval  23565  lmbrf  23593  cnconst2  23616  conncompcld  23767  hauspwdom  23835  txuni2  23899  xkouni  23933  xkoccn  23953  txkgen  23986  qtoptop2  24033  kqdisj  24066  hmphtop  24112  hmpher  24118  uzrest  24231  uzfbas  24232  lmflf  24339  tgpconncompeqg  24446  tgpconncomp  24447  ustn0  24555  xmeter  24767  isngp2  24931  xrtgioo  25141  iccntr  25156  xmetdcn  25173  metdcn  25175  metdscn2  25192  cnheiborlem  25290  reparphti  25333  lmmbrf  25598  iscau4  25615  iscauf  25616  caucfil  25619  lmclimf  25640  volf  25865  uniioombllem3  25921  uniioombllem4  25922  uniioombllem5  25923  volcn  25942  mbfimaopnlem  25991  mbflimsup  26002  i1f1  26026  itg2lcl  26063  itgioo  26151  itgsplitioo  26173  limcflflem  26215  limcflf  26216  limcresi  26220  lhop  26351  dvfsumlem1  26361  dvfsumlem2  26362  dvfsumlem3  26363  dvfsumlem4  26364  dvfsumrlimge0  26365  dvfsumrlim  26366  dvfsumrlim2  26367  dvfsum2  26369  vieta1lem1  26648  vieta1lem2  26649  psercnlem2  26766  psercnlem1  26767  psercn  26768  pserdvlem1  26769  pserdvlem2  26770  pserdv  26771  pserdv2  26772  logcnlem5  26989  dvlog  26994  dvlog2lem  26995  dvlog2  26996  dvcncxp1  27086  dvcnsqrt  27087  cxpcn3lem  27090  cxpcn3  27091  sqrtcn  27093  1cubr  27185  atansssdm  27276  jensen  27331  musum  27533  ppiub  27546  lgsquadlem1  27722  lgsquadlem2  27723  lgsquadlem3  27724  2sqlem7  27766  nosupbnd1lem1  28080  nosupbnd2  28088  noinfbnd1lem1  28095  cutsf  28193  leftssold  28272  rightssold  28273  mulsproplem12  28528  mulsproplem13  28529  mulsproplem14  28530  precsexlem8  28615  onssno  28655  nnssn0s  28722  dfnns2  28773  bdaypw2n0bndlem  28864  axtgcgrrflx  28939  axtgcgrid  28940  axtgsegcon  28941  axtg5seg  28942  axtgbtwnid  28943  axtgpasch  28944  axtgcont1  28945  tglng  29024  disjxwwlkn  30517  frgrwopreg2  30935  phnv  31431  htthlem  31534  hlimadd  31810  hlimcaui  31853  hhsscms  31895  occllem  31920  shjshsi  32109  3oalem4  32282  pjfi  32321  dmadjss  32504  nlelshi  32677  nlelchi  32678  hmopidmchi  32768  shatomistici  32978  difxp1ss  33175  difxp2ss  33176  fcoinver  33255  opabssi  33264  mptctf  33365  ccatws1f1o  33570  gsumpart  33680  pmtrcnel2  33707  psgnfzto1stlem  33717  cycpmrn  33760  cyc3genpm  33769  unitprodclb  34000  lsmsnorb  34002  ply1degltel  34182  ply1degleel  34183  ply1degltlss  34184  evlextv  34230  vietalem  34267  constrsscn  34428  cnre2csqima  34599  raddcn  34617  zrhcntr  34667  rrhre  34709  esumsnf  34752  sxbrsiga  34978  omssubadd  34988  carsggect  35006  sitmcl  35039  oddpwdc  35042  eulerpartlem1  35055  eulerpartlemt  35059  eulerpartgbij  35060  eulerpartlemmf  35063  eulerpartlemgh  35066  sseqf  35080  ballotlemfmpn  35183  ballotth  35226  signswch  35246  ftc2re  35283  fdvposlt  35284  fdvposle  35286  bnj1146  35477  bnj1292  35501  bnj1293  35502  bnj1145  35679  bnj1177  35692  fineqvnttrclse  35866  tz9.1regs  35876  dmr0ss  35959  erdszelem2  36081  kur14lem3  36097  kur14lem6  36100  kur14lem7  36101  kur14lem9  36103  cvmlift2lem12  36203  mpstssv  36428  mstapst  36436  mppspstlem  36460  mppspst  36463  mthmsta  36467  mthmpps  36471  mclsppslem  36472  txpss3v  36770  pprodss4v  36776  relsset  36780  fixssdm  36798  fixssrn  36799  limitssson  36803  funpartss  36838  colinearex  36955  fneer  37271  neibastop1  37277  neibastop2lem  37278  filnetlem2  37297  filnetlem3  37298  ttcuniun  37428  ttcuni  37431  knoppcnlem10  37498  bj-tagss  38023  bj-resss2  38093  bj-imdirco  38254  bj-fvsnun2  38320  bj-ablssgrp  38340  bj-ablsscmn  38342  bj-vecssmod  38345  bj-fldssdrng  38352  icoreresf  38418  icoreunrn  38425  poimirlem29  38710  poimirlem30  38711  poimirlem31  38712  poimir  38714  broucube  38715  dvasin  38765  dvacos  38766  areacirc  38774  caures  38837  bnd2lem  38868  ismtyres  38885  flddivrng  39076  xrnss3v  39456  refrelsredund2  39792  toycom  40173  dihglblem2N  42494  lcdvbase  42793  mapdunirnN  42850  aks6d1c1p1rcl  43301  redvmptabs  43554  readvrec  43556  prjspreln0  43780  prjspvs  43781  prjspeclsp  43783  frlmnzcoordcl2  43799  prjspnnorm  43804  0prjspnrel  43806  dffltz  43813  eldiophb  43911  monotuz  44091  pwssplit4  44234  pwfi2f1o  44241  arearect  44360  cantnfresb  44469  omabs2  44477  fvnonrel  44740  rclexi  44758  rtrclex  44760  trclexi  44763  rtrclexi  44764  clcnvlem  44766  cnvrcl0  44768  cnvtrcl0  44769  dfrtrcl5  44772  dfrcl2  44817  comptiunov2i  44849  corclrcl  44850  trclrelexplem  44854  relexpaddss  44861  cotrcltrcl  44868  corcltrcl  44882  cotrclrcl  44885  frege131d  44907  0he  44925  grumnudlem  45412  uzmptshftfval  45473  binomcxplemdvbinom  45480  binomcxplemdvsum  45482  binomcxplemnotnn0  45483  modelaxreplem2  46111  rabexgf  46183  uzct  46222  disjf1o  46348  dmmptssf  46386  mptssid  46395  uzfissfz  46480  ssuzfz  46503  uzssre2  46559  uzublem  46582  uzssz2  46608  uzsscn2  46629  sumnnodd  46784  climconstmpt  46810  fnlimfvre  46826  fnlimabslt  46831  limsupubuzlem  46864  limsupubuz  46865  limsupequzmpt2  46870  limsupmnfuzlem  46878  limsupre3uzlem  46887  liminfequzmpt2  46943  ibliooicc  47123  stoweidlem44  47196  stoweidlem50  47202  stoweidlem51  47203  stoweidlem52  47204  stoweidlem57  47209  stoweidlem59  47211  fourierdlem16  47275  fourierdlem19  47278  fourierdlem21  47280  fourierdlem22  47281  fourierdlem42  47301  fourierdlem83  47341  fouriersw  47383  salexct  47486  salexct3  47494  salgencntex  47495  salgensscntex  47496  sge0less  47544  sge0fodjrnlem  47568  sge0isum  47579  ovnlerp  47714  ovn0lem  47717  hoidmv1lelem1  47743  hoidmv1lelem3  47745  hoidmvlelem1  47747  hoidmvlelem2  47748  hoidmvlelem3  47749  hoidmvlelem4  47750  ovnhoilem1  47753  ovnhoilem2  47754  opnvonmbllem2  47785  ovolval4lem1  47801  ovolval5lem3  47806  pimdecfgtioc  47867  pimincfltioc  47868  pimdecfgtioo  47869  pimincfltioo  47870  incsmflem  47893  decsmflem  47918  smflimlem2  47924  smflimlem3  47925  smflim  47929  smfrec  47941  smfmullem4  47946  smfdiv  47949  smfsuplem1  47963  smfsuplem3  47965  smfsupxr  47968  smfliminflem  47982  cfsetssfset  48268  fcoreslem2  48276  fcores  48279  gricrel  49159  clnbgrisubgrgrim  49172  isubgr3stgrlem6  49211  isubgr3stgrlem7  49212  isubgr3stgrlem8  49213  isubgr3stgr  49215  grlimgrtrilem2  49242  grlicrel  49246  oddibas  49412  2zlidl  49479  2zrngbas  49481  2zrng0  49483  fldcALTV  49571  fldhmsubcALTV  49572  dmtposss  50131  tposres3  50136  ipolub0  50248  imaidfu  50368  parhomssun  50889