Theorem eqsstri 3975

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3914

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3915

This theorem is used by:  eqsstrri  3976  3sstr4i  3980  ssrab3  4028  rabssab  4031  ifssun  4500  opabss  5169  brab2a  5744  relopabiALT  5801  dmopabss  5900  rnopabss  5937  resss  5992  relres  5996  rninOLD  6138  rnxpss  6164  cnvcnvss  6186  cnvcnvssOLD  6187  resdmss  6237  resssxp  6273  dfpo2  6300  predss  6313  fnres  6667  f0  6764  nfvres  6924  fvopab4ndm  7025  ffvresb  7127  mptexgf  7229  funiunfv  7253  isoini2  7348  ovssunirn  7457  dmoprabss  7525  mpondm0  7662  elmpocl  7663  exse2  7930  frxp  8139  tposssxp  8248  dftpos4  8263  smores  8361  smores2  8363  iordsmo  8366  swoer  8750  swoord1  8751  swoord2  8752  ecss  8770  ecopovsym  8841  ecopovtrn  8842  ecopover  8843  f1setex  8880  sbthlem7  9113  imafi  9308  elfiun  9423  marypha1lem  9426  marypha2lem1  9428  hartogslem1  9537  wdomima2g  9581  inf3lem1  9630  dmttrcl  9723  rnttrcl  9724  tc2  9742  frmin  9754  frrlem16  9763  frr1  9764  tz9.12lem1  9795  rankuni  9880  rankuniss  9884  rankmapu  9896  hta  9963  htaOLD  9964  r0weon  10092  infxpenlem  10093  ackbij1lem9  10306  ackbij1lem10  10307  ackbij1b  10317  sdom2en01  10381  fin23lem26  10404  fin56  10472  fin1a2lem9  10487  axdc3lem  10529  axdc3lem2  10530  axcclem  10536  imadomg  10614  iundom2g  10625  smobeth  10672  canth4  10733  gruina  10904  grur1a  10905  pinn  10964  niex  10967  ltsopi  10974  ltrelpi  10975  dmaddpi  10976  dmmulpi  10977  enqex  11008  ltrelnq  11012  nqerf  11016  nqerrel  11018  dmrecnq  11054  lterpq  11056  ltrelpr  11084  enrex  11153  ltrelsr  11154  dmaddsr  11171  dmmulsr  11172  ltrelre  11220  axaddf  11231  axmulf  11232  ltrelxr  11371  lerelxr  11373  nn0ssre  12611  nn0sscn  12612  nn0ssz  12717  uzsupss  13068  rpnnen1lem1  13107  rpnnen1lem3  13108  rpnnen1lem5  13110  fz1ssfz0  13758  uzsup  14004  fzfi  14116  swrd00  14793  01sqrexlem3  15412  cau3  15524  caubnd  15527  limsupgre  15649  rlimpm  15668  rlimclim  15714  isercolllem1  15833  isercolllem2  15834  isercoll  15836  caurcvg  15845  caucvg  15847  iseraltlem2  15851  iseraltlem3  15852  zsum  15885  fsumcvg3  15896  climfsum  15988  ackbijnn  15998  divcnvshft  16025  infcvgaux1i  16027  clim2prod  16058  ntrivcvg  16067  ntrivcvgfvn0  16069  ntrivcvgtail  16070  ntrivcvgmullem  16071  ntrivcvgmul  16072  zprod  16105  dvdszrcl  16428  4sqlem1  17127  4sqlem19  17142  ramub1lem2  17206  structcnvcnv  17332  strleun  17336  fvsetsid  17347  idressidex0  18861  smndex1sgrp  19108  gicer  19492  cntzsgrpcl  19549  symgbasfi  19594  mvdco  19660  symgsssg  19682  efglem  19931  efgtf  19937  efgtlen  19941  efginvrel2  19942  efginvrel1  19943  efgsfo  19954  efgredlemg  19957  efgredleme  19958  efgredlemd  19959  efgredlemc  19960  efgredlem  19962  efgred  19963  efgrelexlemb  19965  efgcpbllemb  19970  frgpinv  19979  frgpuplem  19987  frgpupf  19988  frgpup1  19990  frgpnabllem2  20089  gsumval3lem1  20120  gsumval3lem2  20121  gsumval3  20122  ricrel  20745  fldc  21042  fldhmsubc  21043  lbsextlem3  21439  pzriprnglem10  21797  znf1o  21858  zntoslem  21863  pjpm  22015  mhp0cl  22468  ply1bascl  22522  dmtopon  23242  ordtbas  23511  leordtval2  23531  lecldbas  23538  lmfval  23551  lmbrf  23579  cnconst2  23602  conncompcld  23753  hauspwdom  23821  txuni2  23885  xkouni  23919  xkoccn  23939  txkgen  23972  qtoptop2  24019  kqdisj  24052  hmphtop  24098  hmpher  24104  uzrest  24217  uzfbas  24218  lmflf  24325  tgpconncompeqg  24432  tgpconncomp  24433  ustn0  24541  xmeter  24753  isngp2  24917  xrtgioo  25127  iccntr  25142  xmetdcn  25159  metdcn  25161  metdscn2  25178  cnheiborlem  25276  reparphti  25319  lmmbrf  25584  iscau4  25601  iscauf  25602  caucfil  25605  lmclimf  25626  volf  25851  uniioombllem3  25907  uniioombllem4  25908  uniioombllem5  25909  volcn  25928  mbfimaopnlem  25977  mbflimsup  25988  i1f1  26012  itg2lcl  26049  itgioo  26137  itgsplitioo  26159  limcflflem  26201  limcflf  26202  limcresi  26206  lhop  26337  dvfsumlem1  26347  dvfsumlem2  26348  dvfsumlem3  26349  dvfsumlem4  26350  dvfsumrlimge0  26351  dvfsumrlim  26352  dvfsumrlim2  26353  dvfsum2  26355  vieta1lem1  26634  vieta1lem2  26635  psercnlem2  26752  psercnlem1  26753  psercn  26754  pserdvlem1  26755  pserdvlem2  26756  pserdv  26757  pserdv2  26758  logcnlem5  26975  dvlog  26980  dvlog2lem  26981  dvlog2  26982  dvcncxp1  27072  dvcnsqrt  27073  cxpcn3lem  27076  cxpcn3  27077  sqrtcn  27079  1cubr  27171  atansssdm  27262  jensen  27317  musum  27519  ppiub  27532  lgsquadlem1  27708  lgsquadlem2  27709  lgsquadlem3  27710  2sqlem7  27752  nosupbnd1lem1  28066  nosupbnd2  28074  noinfbnd1lem1  28081  cutsf  28179  leftssold  28258  rightssold  28259  mulsproplem12  28514  mulsproplem13  28515  mulsproplem14  28516  precsexlem8  28601  onssno  28641  nnssn0s  28708  dfnns2  28759  bdaypw2n0bndlem  28850  axtgcgrrflx  28925  axtgcgrid  28926  axtgsegcon  28927  axtg5seg  28928  axtgbtwnid  28929  axtgpasch  28930  axtgcont1  28931  tglng  29010  disjxwwlkn  30503  frgrwopreg2  30921  phnv  31417  htthlem  31520  hlimadd  31796  hlimcaui  31839  hhsscms  31881  occllem  31906  shjshsi  32095  3oalem4  32268  pjfi  32307  dmadjss  32490  nlelshi  32663  nlelchi  32664  hmopidmchi  32754  shatomistici  32964  difxp1ss  33119  difxp2ss  33120  fcoinver  33199  opabssi  33208  mptctf  33309  ccatws1f1o  33515  gsumpart  33625  pmtrcnel2  33652  psgnfzto1stlem  33662  cycpmrn  33705  cyc3genpm  33714  unitprodclb  33945  lsmsnorb  33947  ply1degltel  34127  ply1degleel  34128  ply1degltlss  34129  evlextv  34175  vietalem  34212  constrsscn  34373  cnre2csqima  34544  raddcn  34562  zrhcntr  34612  rrhre  34654  esumsnf  34697  sxbrsiga  34923  omssubadd  34933  carsggect  34951  sitmcl  34984  oddpwdc  34987  eulerpartlem1  35000  eulerpartlemt  35004  eulerpartgbij  35005  eulerpartlemmf  35008  eulerpartlemgh  35011  sseqf  35025  ballotlemfmpn  35128  ballotth  35171  signswch  35191  ftc2re  35228  fdvposlt  35229  fdvposle  35231  bnj1146  35422  bnj1292  35446  bnj1293  35447  bnj1145  35624  bnj1177  35637  fineqvnttrclse  35793  tz9.1regs  35803  erdszelem2  35958  kur14lem3  35974  kur14lem6  35977  kur14lem7  35978  kur14lem9  35980  cvmlift2lem12  36080  mpstssv  36305  mstapst  36313  mppspstlem  36337  mppspst  36340  mthmsta  36344  mthmpps  36348  mclsppslem  36349  txpss3v  36641  pprodss4v  36647  relsset  36651  fixssdm  36669  fixssrn  36670  limitssson  36674  funpartss  36709  colinearex  36826  fneer  37142  neibastop1  37148  neibastop2lem  37149  filnetlem2  37168  filnetlem3  37169  ttcuniun  37299  ttcuni  37302  knoppcnlem10  37369  bj-tagss  37894  bj-imdirco  38113  bj-fvsnun2  38179  bj-ablssgrp  38199  bj-ablsscmn  38201  bj-vecssmod  38204  bj-fldssdrng  38211  icoreresf  38277  icoreunrn  38284  poimirlem29  38569  poimirlem30  38570  poimirlem31  38571  poimir  38573  broucube  38574  dvasin  38624  dvacos  38625  areacirc  38633  caures  38696  bnd2lem  38727  ismtyres  38744  flddivrng  38935  xrnss3v  39315  refrelsredund2  39651  toycom  40032  dihglblem2N  42353  lcdvbase  42652  mapdunirnN  42709  aks6d1c1p1rcl  43160  redvmptabs  43413  readvrec  43415  prjspreln0  43639  prjspvs  43640  prjspeclsp  43642  frlmnzcoordcl2  43658  prjspnnorm  43663  0prjspnrel  43665  dffltz  43672  eldiophb  43769  monotuz  43949  pwssplit4  44092  pwfi2f1o  44099  arearect  44218  cantnfresb  44327  omabs2  44335  fvnonrel  44598  rclexi  44616  rtrclex  44618  trclexi  44621  rtrclexi  44622  clcnvlem  44624  cnvrcl0  44626  cnvtrcl0  44627  dfrtrcl5  44630  dfrcl2  44675  comptiunov2i  44707  corclrcl  44708  trclrelexplem  44712  relexpaddss  44719  cotrcltrcl  44726  corcltrcl  44740  cotrclrcl  44743  frege131d  44765  0he  44783  grumnudlem  45270  uzmptshftfval  45331  binomcxplemdvbinom  45338  binomcxplemdvsum  45340  binomcxplemnotnn0  45341  modelaxreplem2  45970  rabexgf  46042  uzct  46081  disjf1o  46207  dmmptssf  46245  mptssid  46254  uzfissfz  46339  ssuzfz  46362  uzssre2  46418  uzublem  46441  uzssz2  46467  uzsscn2  46488  sumnnodd  46643  climconstmpt  46669  fnlimfvre  46685  fnlimabslt  46690  limsupubuzlem  46723  limsupubuz  46724  limsupequzmpt2  46729  limsupmnfuzlem  46737  limsupre3uzlem  46746  liminfequzmpt2  46802  ibliooicc  46982  stoweidlem44  47055  stoweidlem50  47061  stoweidlem51  47062  stoweidlem52  47063  stoweidlem57  47068  stoweidlem59  47070  fourierdlem16  47134  fourierdlem19  47137  fourierdlem21  47139  fourierdlem22  47140  fourierdlem42  47160  fourierdlem83  47200  fouriersw  47242  salexct  47345  salexct3  47353  salgencntex  47354  salgensscntex  47355  sge0less  47403  sge0fodjrnlem  47427  sge0isum  47438  ovnlerp  47573  ovn0lem  47576  hoidmv1lelem1  47602  hoidmv1lelem3  47604  hoidmvlelem1  47606  hoidmvlelem2  47607  hoidmvlelem3  47608  hoidmvlelem4  47609  ovnhoilem1  47612  ovnhoilem2  47613  opnvonmbllem2  47644  ovolval4lem1  47660  ovolval5lem3  47665  pimdecfgtioc  47726  pimincfltioc  47727  pimdecfgtioo  47728  pimincfltioo  47729  incsmflem  47752  decsmflem  47777  smflimlem2  47783  smflimlem3  47784  smflim  47788  smfrec  47800  smfmullem4  47805  smfdiv  47808  smfsuplem1  47822  smfsuplem3  47824  smfsupxr  47827  smfliminflem  47841  cfsetssfset  48127  fcoreslem2  48135  fcores  48138  gricrel  49018  clnbgrisubgrgrim  49031  isubgr3stgrlem6  49070  isubgr3stgrlem7  49071  isubgr3stgrlem8  49072  isubgr3stgr  49074  grlimgrtrilem2  49101  grlicrel  49105  oddibas  49271  2zlidl  49338  2zrngbas  49340  2zrng0  49342  fldcALTV  49430  fldhmsubcALTV  49431  dmtposss  49985  tposres3  49990  ipolub0  50101  imaidfu  50219