Theorem eqsstri 4017

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

Syntax hints:   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqsstrri  4018  ssrab2OLD  4079  ssrab3  4081  rabssab  4084  ifssun  4546  opabss  5213  brab2a  5770  relopabiALT  5824  dmopabss  5919  resss  6007  relres  6011  rnin  6147  rnxpss  6172  cnvcnvss  6194  resdmss  6235  resssxp  6270  dfpo2  6296  predss  6309  fnres  6678  f0  6773  nfvres  6933  fvopab4ndm  7028  ffvresb  7124  mptexgf  7224  funiunfv  7247  isoini2  7336  ovssunirn  7445  dmoprabss  7511  mpondm0  7647  elmpocl  7648  exse2  7908  fabexg  7925  frxp  8112  tposssxp  8215  dftpos4  8230  wfrdmssOLD  8315  smores  8352  smores2  8354  iordsmo  8357  swoer  8733  swoord1  8734  swoord2  8735  ecss  8749  ecopovsym  8813  ecopovtrn  8814  ecopover  8815  f1setex  8851  sbthlem7  9089  nnfiOLD  9232  imafiALT  9345  elfiun  9425  marypha1lem  9428  marypha2lem1  9430  hartogslem1  9537  wdomima2g  9581  inf3lem1  9623  dmttrcl  9716  rnttrcl  9717  tc2  9737  frmin  9744  frrlem16  9753  frr1  9754  tz9.12lem1  9782  rankuni  9858  rankuniss  9861  rankmapu  9873  hta  9892  r0weon  10007  infxpenlem  10008  ackbij1lem9  10223  ackbij1lem10  10224  ackbij1b  10234  sdom2en01  10297  fin23lem26  10320  fin56  10388  fin1a2lem9  10403  axdc3lem  10445  axdc3lem2  10446  axcclem  10452  imadomg  10529  iundom2g  10535  smobeth  10581  canth4  10642  gruina  10813  grur1a  10814  pinn  10873  niex  10876  ltsopi  10883  ltrelpi  10884  dmaddpi  10885  dmmulpi  10886  enqex  10917  ltrelnq  10921  nqerf  10925  nqerrel  10927  dmrecnq  10963  lterpq  10965  ltrelpr  10993  enrex  11062  ltrelsr  11063  dmaddsr  11080  dmmulsr  11081  ltrelre  11129  axaddf  11140  axmulf  11141  ltrelxr  11275  lerelxr  11277  nn0ssre  12476  nn0sscn  12477  nn0ssz  12581  uzsupss  12924  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  fz1ssfz0  13597  uzsup  13828  fzfi  13937  swrd00  14594  01sqrexlem3  15191  cau3  15302  caubnd  15305  limsupgre  15425  rlimpm  15444  rlimclim  15490  isercolllem1  15611  isercolllem2  15612  isercoll  15614  caurcvg  15623  caucvg  15625  iseraltlem2  15629  iseraltlem3  15630  zsum  15664  fsumcvg3  15675  climfsum  15766  ackbijnn  15774  divcnvshft  15801  infcvgaux1i  15803  clim2prod  15834  ntrivcvg  15843  ntrivcvgfvn0  15845  ntrivcvgtail  15846  ntrivcvgmullem  15847  ntrivcvgmul  15848  zprod  15881  dvdszrcl  16202  4sqlem1  16881  4sqlem19  16896  ramub1lem2  16960  structcnvcnv  17086  strleun  17090  fvsetsid  17101  smndex1sgrp  18789  gicer  19150  cntzsgrpcl  19198  symgbasfi  19246  mvdco  19313  symgsssg  19335  efglem  19584  efgtf  19590  efgtlen  19594  efginvrel2  19595  efginvrel1  19596  efgsfo  19607  efgredlemg  19610  efgredleme  19611  efgredlemd  19612  efgredlemc  19613  efgredlem  19615  efgred  19616  efgrelexlemb  19618  efgcpbllemb  19623  frgpinv  19632  frgpuplem  19640  frgpupf  19641  frgpup1  19643  frgpnabllem2  19742  gsumval3lem1  19773  gsumval3lem2  19774  gsumval3  19775  lbsextlem3  20773  znf1o  21107  zntoslem  21112  pjpm  21263  mhp0cl  21689  ply1bascl  21727  dmtopon  22425  ordtbas  22696  leordtval2  22716  lecldbas  22723  lmfval  22736  lmbrf  22764  cnconst2  22787  conncompcld  22938  hauspwdom  23005  txuni2  23069  xkouni  23103  xkoccn  23123  txkgen  23156  qtoptop2  23203  kqdisj  23236  hmphtop  23282  hmpher  23288  uzrest  23401  uzfbas  23402  lmflf  23509  tgpconncompeqg  23616  tgpconncomp  23617  ustn0  23725  xmeter  23939  isngp2  24106  xrtgioo  24322  iccntr  24337  xmetdcn  24354  metdcn  24356  metdscn2  24373  icchmeo  24457  cnheiborlem  24470  lmmbrf  24779  iscau4  24796  iscauf  24797  caucfil  24800  lmclimf  24821  volf  25046  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  volcn  25123  mbfimaopnlem  25172  mbflimsup  25183  i1f1  25207  itg2lcl  25245  itgioo  25333  itgsplitioo  25355  limcflflem  25397  limcflf  25398  limcresi  25402  lhop  25533  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlimge0  25547  dvfsumrlim  25548  dvfsumrlim2  25549  dvfsum2  25551  vieta1lem1  25823  vieta1lem2  25824  psercnlem2  25936  psercnlem1  25937  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  pserdv  25941  pserdv2  25942  logcnlem5  26154  dvlog  26159  dvlog2lem  26160  dvlog2  26161  dvcncxp1  26251  dvcnsqrt  26252  cxpcn3lem  26255  cxpcn3  26256  sqrtcn  26258  1cubr  26347  atansssdm  26438  jensen  26493  musum  26695  ppiub  26707  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  2sqlem7  26927  nosupbnd1lem1  27211  nosupbnd2  27219  noinfbnd1lem1  27226  scutf  27313  leftssold  27373  rightssold  27374  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  precsexlem8  27660  axtgcgrrflx  27713  axtgcgrid  27714  axtgsegcon  27715  axtg5seg  27716  axtgbtwnid  27717  axtgpasch  27718  axtgcont1  27719  tglng  27797  disjxwwlkn  29167  frgrwopreg2  29572  phnv  30067  htthlem  30170  hlimadd  30446  hlimcaui  30489  hhsscms  30531  occllem  30556  shjshsi  30745  3oalem4  30918  pjfi  30957  dmadjss  31140  nlelshi  31313  nlelchi  31314  hmopidmchi  31404  shatomistici  31614  difxp1ss  31760  difxp2ss  31761  fcoinver  31835  opabssi  31842  mptctf  31942  gsumpart  32207  pmtrcnel2  32251  psgnfzto1stlem  32259  cycpmrn  32302  cyc3genpm  32311  lsmsnorb  32501  ply1degltel  32666  ply1degltlss  32667  cnre2csqima  32891  raddcn  32909  rrhre  33001  esumsnf  33062  sxbrsiga  33289  omssubadd  33299  carsggect  33317  sitmcl  33350  oddpwdc  33353  eulerpartlem1  33366  eulerpartlemt  33370  eulerpartgbij  33371  eulerpartlemmf  33374  eulerpartlemgh  33377  sseqf  33391  ballotlemfmpn  33493  ballotth  33536  signswch  33572  ftc2re  33610  fdvposlt  33611  fdvposle  33613  bnj1146  33802  bnj1292  33826  bnj1293  33827  bnj1145  34004  bnj1177  34017  erdszelem2  34183  kur14lem3  34199  kur14lem6  34202  kur14lem7  34203  kur14lem9  34205  cvmlift2lem12  34305  mpstssv  34530  mstapst  34538  mppspstlem  34562  mppspst  34565  mthmsta  34569  mthmpps  34573  mclsppslem  34574  txpss3v  34850  pprodss4v  34856  relsset  34860  fixssdm  34878  fixssrn  34879  limitssson  34883  funpartss  34916  colinearex  35032  gg-reparphti  35172  gg-dvfsumlem2  35183  fneer  35238  neibastop1  35244  neibastop2lem  35245  filnetlem2  35264  filnetlem3  35265  knoppcnlem10  35378  bj-tagss  35861  bj-imdirco  36071  bj-fvsnun2  36137  bj-ablssgrp  36157  bj-ablsscmn  36159  bj-vecssmod  36162  bj-fldssdrng  36169  icoreresf  36233  icoreunrn  36240  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimir  36521  broucube  36522  dvasin  36572  dvacos  36573  areacirc  36581  caures  36628  bnd2lem  36659  ismtyres  36676  flddivrng  36867  xrnss3v  37242  refrelsredund2  37503  toycom  37843  dihglblem2N  40165  lcdvbase  40464  mapdunirnN  40521  prjspreln0  41351  prjspvs  41352  prjspeclsp  41354  0prjspnrel  41369  dffltz  41376  eldiophb  41495  monotuz  41680  pwssplit4  41831  pwfi2f1o  41838  arearect  41964  cantnfresb  42074  omabs2  42082  fvnonrel  42348  rclexi  42366  rtrclex  42368  trclexi  42371  rtrclexi  42372  clcnvlem  42374  cnvrcl0  42376  cnvtrcl0  42377  dfrtrcl5  42380  dfrcl2  42425  comptiunov2i  42457  corclrcl  42458  trclrelexplem  42462  relexpaddss  42469  cotrcltrcl  42476  corcltrcl  42490  cotrclrcl  42493  frege131d  42515  0he  42533  grumnudlem  43044  uzmptshftfval  43105  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  rabexgf  43708  uzct  43750  disjf1o  43889  dmresss  43933  dmmptssf  43934  mptssid  43944  uzfissfz  44036  ssuzfz  44059  uzssre2  44117  uzublem  44140  uzssz2  44166  uzsscn2  44188  sumnnodd  44346  climconstmpt  44374  fnlimfvre  44390  fnlimabslt  44395  limsupvaluz  44424  limsupubuzlem  44428  limsupubuz  44429  limsupequzmpt2  44434  limsupmnfuzlem  44442  limsupre3uzlem  44451  liminfequzmpt2  44507  ibliooicc  44687  stoweidlem44  44760  stoweidlem50  44766  stoweidlem51  44767  stoweidlem52  44768  stoweidlem57  44773  stoweidlem59  44775  fourierdlem16  44839  fourierdlem19  44842  fourierdlem21  44844  fourierdlem22  44845  fourierdlem42  44865  fourierdlem83  44905  fouriersw  44947  salexct  45050  salexct3  45058  salgencntex  45059  salgensscntex  45060  sge0less  45108  sge0fodjrnlem  45132  sge0isum  45143  ovnlerp  45278  ovn0lem  45281  hoidmv1lelem1  45307  hoidmv1lelem3  45309  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  ovnhoilem1  45317  ovnhoilem2  45318  opnvonmbllem2  45349  ovolval4lem1  45365  ovolval5lem3  45370  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  incsmflem  45457  decsmflem  45482  smflimlem2  45488  smflimlem3  45489  smflim  45493  smfrec  45505  smfmullem4  45510  smfdiv  45513  smfsuplem1  45527  smfsuplem3  45529  smfsupxr  45532  smfliminflem  45546  cfsetssfset  45766  fcoreslem2  45774  fcores  45777  oddibas  46583  pzriprnglem10  46814  2zlidl  46832  2zrngbas  46834  2zrng0  46836  fldc  46981  fldhmsubc  46982  fldcALTV  46999  fldhmsubcALTV  47000  ipolub0  47617