Theorem eqsstri 3598

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

Syntax hints:   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  eqsstr3i  3599  ssrab2  3650  rabssab  3652  opabss  4646  brab2ga  5117  relopabiALT  5168  dmopabss  5258  resss  5342  relres  5346  rnin  5461  rnxpss  5485  cnvcnvss  5507  dmmptss  5548  predss  5604  fnres  5921  f0  5999  nfvres  6134  fvopab4ndm  6215  ffvresb  6301  funiunfv  6410  isoini2  6489  ovssunirn  6579  dmoprabss  6640  mpt2ndm0  6773  elmpt2cl  6774  omsson  6961  exse2  6998  fabexg  7015  frxp  7174  tposssxp  7243  dftpos4  7258  wfrdmss  7308  smores  7336  smores2  7338  iordsmo  7341  oawordeulem  7521  swoer  7659  swoord1  7660  swoord2  7661  ecss  7675  ecopovsym  7736  ecopovtrn  7737  ecopover  7738  ecopoverOLD  7739  sbthlem7  7961  nnfi  8038  imafi  8142  elfiun  8219  marypha1lem  8222  marypha2lem1  8224  ordtypelem2  8307  hartogslem1  8330  wemapso2lem  8340  wdomima2g  8374  inf3lem1  8408  wemapwe  8477  tc2  8501  tz9.12lem1  8533  rankuni  8609  rankuniss  8612  rankmapu  8624  cplem1  8635  hta  8643  r0weon  8718  infxpenlem  8719  ackbij1lem9  8933  ackbij1lem10  8934  ackbij1b  8944  cofsmo  8974  sdom2en01  9007  fin23lem26  9030  fin23lem28  9045  fin23lem30  9047  isf32lem5  9062  isf32lem6  9063  isf32lem7  9064  isf32lem8  9065  fin56  9098  fin1a2lem9  9113  hsmexlem4  9134  hsmexlem5  9135  hsmexlem6  9136  axdc3lem  9155  axdc3lem2  9156  axcclem  9162  zorn2lem1  9201  zorn2lem3  9203  zorn2lem4  9204  zorn2lem5  9205  imadomg  9237  iundom2g  9241  smobeth  9287  canth4  9348  gruina  9519  grur1a  9520  pinn  9579  niex  9582  ltsopi  9589  ltrelpi  9590  dmaddpi  9591  dmmulpi  9592  enqex  9623  0nnq  9625  elpqn  9626  ltrelnq  9627  nqerf  9631  nqerrel  9633  dmrecnq  9669  lterpq  9671  ltrelpr  9699  enrex  9767  ltrelsr  9768  dmaddsr  9785  dmmulsr  9786  ltrelre  9834  axaddf  9845  axmulf  9846  ltrelxr  9978  lerelxr  9980  nn0ssre  11173  nn0ssz  11275  uzsupss  11656  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  rpre  11715  uzsup  12524  fzfi  12633  swrd00  13270  sqrlem3  13833  sqrlem5  13835  cau3  13943  caubnd  13946  limsupgre  14060  rlimpm  14079  rlimclim  14125  isercolllem1  14243  isercolllem2  14244  isercoll  14246  caurcvg  14255  caucvg  14257  iseraltlem2  14261  iseraltlem3  14262  zsum  14296  fsumcvg3  14307  climfsum  14393  ackbijnn  14399  divcnvshft  14426  infcvgaux1i  14428  clim2prod  14459  ntrivcvg  14468  ntrivcvgfvn0  14470  ntrivcvgtail  14471  ntrivcvgmullem  14472  ntrivcvgmul  14473  zprod  14506  dvdszrcl  14826  dvdsflip  14877  divalglem2  14956  divalglem5  14958  divalglem8  14961  gcdcllem3  15061  bezoutlem2  15095  bezoutlem3  15096  maxprmfct  15259  phimullem  15322  eulerthlem2  15325  prmdiveq  15329  prmdivdiv  15330  pclem  15381  infpn2  15455  prmreclem2  15459  prmreclem3  15460  prmreclem5  15462  4sqlem1  15490  4sqlem13  15499  4sqlem14  15500  4sqlem17  15503  4sqlem18  15504  4sqlem19  15505  vdwnnlem3  15539  ramcl2lem  15551  ramtcl  15552  ramtcl2  15553  ramtub  15554  ramub1lem2  15569  structcnvcnv  15706  fvsetsid  15722  strlemor0  15795  strlemor1  15796  strleun  15799  imasdsval2  15999  gsumval1  17100  nmzsubg  17458  nmznsg  17461  conjnmz  17517  conjnmzb  17518  gicer  17541  gicerOLD  17542  gastacl  17565  symgbasfi  17629  mvdco  17688  symgsssg  17710  sylow1lem2  17837  sylow1lem3  17838  sylow1lem4  17839  sylow1lem5  17840  sylow2a  17857  sylow3lem2  17866  efglem  17952  efgtf  17958  efgtlen  17962  efginvrel2  17963  efginvrel1  17964  efgsfo  17975  efgredlemg  17978  efgredleme  17979  efgredlemd  17980  efgredlemc  17981  efgredlem  17983  efgred  17984  efgrelexlemb  17986  efgcpbllemb  17991  frgpinv  18000  frgpuplem  18008  frgpupf  18009  frgpup1  18011  frgpnabllem2  18100  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  ablfacrplem  18287  ablfacrp2  18289  ablfac1eu  18295  pgpfaclem1  18303  ablfaclem2  18308  ablfaclem3  18309  lspsolvlem  18963  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  rrgeq0  19111  rrgss  19113  psrbagconf1o  19195  psrass1lem  19198  mplbasss  19253  ply1bascl  19394  coe1mul2lem2  19459  znf1o  19719  zntoslem  19724  cygznlem2a  19735  psgnghm  19745  pjpm  19871  dsmmbase  19898  frlmsslsp  19954  mretopd  20706  ordtbas  20806  leordtval2  20826  lecldbas  20833  lmfval  20846  lmbrf  20874  cnconst2  20897  hauscmplem  21019  concompcld  21047  hauspwdom  21114  txuni2  21178  xkouni  21212  xkoccn  21232  txkgen  21265  qtoptop2  21312  kqdisj  21345  hmphtop  21391  hmpher  21397  uzrest  21511  uzfbas  21512  lmflf  21619  ptcmplem1  21666  ptcmplem3  21668  tgpconcompeqg  21725  tgpconcomp  21726  ustn0  21834  imasdsf1olem  21988  xmeter  22048  blcld  22120  isngp2  22211  xrtgioo  22417  iccntr  22432  icccmplem1  22433  icccmplem2  22434  icccmplem3  22435  xmetdcn  22449  metdcn  22451  metdscn2  22468  icchmeo  22548  cnheiborlem  22561  lmmbrf  22868  iscau4  22885  iscauf  22886  caucfil  22889  lmclimf  22910  rrxf  22992  ivthlem1  23027  ivthlem2  23028  ivthlem3  23029  ovolsslem  23059  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicc2  23097  volf  23104  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  dyadmbllem  23173  dyadmbl  23174  volcn  23180  mbfimaopnlem  23228  mbflimsup  23239  i1f1  23263  itg2lcl  23300  iblmbf  23340  itgioo  23388  itgsplitioo  23410  limcflflem  23450  limcflf  23451  limcresi  23455  lhop  23583  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlimge0  23597  dvfsumrlim  23598  dvfsumrlim2  23599  dvfsum2  23601  vieta1lem1  23869  vieta1lem2  23870  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  pserdv  23987  pserdv2  23988  abelthlem4  23992  abelthlem6  23994  abelthlem9  23998  abelth  23999  logcnlem5  24192  dvlog  24197  dvlog2lem  24198  dvlog2  24199  dvcncxp1  24284  dvcnsqrt  24285  cxpcn3lem  24288  cxpcn3  24289  sqrtcn  24291  1cubr  24369  atansssdm  24460  atancn  24463  jensen  24515  lgamucov  24564  lgamucov2  24565  wilthlem1  24594  ftalem3  24601  musum  24717  dvdsmulf1o  24720  fsumdvdsmul  24721  ppiub  24729  lgsfcl2  24828  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  2sqlem7  24949  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrisum0  25009  pntlem3  25098  axtgcgrrflx  25161  axtgcgrid  25162  axtgsegcon  25163  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  tglng  25241  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  axcontlem10  25653  nbgraf1olem1  25970  disjxwwlkn  26273  clwlknclwlkdifnum  26488  frgrawopreg1  26577  frgrawopreg2  26578  phnv  27053  htthlem  27158  hlimadd  27434  hlimcaui  27477  hhsscms  27520  occllem  27546  shjshsi  27735  3oalem4  27908  pjfi  27947  dmadjss  28130  nlelshi  28303  nlelchi  28304  hmopidmchi  28394  atssch  28586  shatomistici  28604  fcoinver  28798  mptexgf  28809  mptctf  28883  fcobijfs  28889  psgnfzto1stlem  29181  cnre2csqima  29285  raddcn  29303  rrhre  29393  esumsnf  29453  sxbrsiga  29679  omssubadd  29689  carsggect  29707  sitmcl  29740  oddpwdc  29743  eulerpartlem1  29756  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgh  29767  sseqf  29781  ballotlemfmpn  29883  ballotth  29926  signswch  29964  bnj21  30037  bnj1146  30116  bnj1292  30140  bnj1293  30141  bnj1145  30315  bnj1177  30328  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem2  30428  kur14lem3  30444  kur14lem6  30447  kur14lem7  30448  kur14lem9  30450  cvmlift2lem12  30550  mpstssv  30690  mstapst  30698  mppspstlem  30722  mppspst  30725  mthmsta  30729  mthmpps  30733  mclsppslem  30734  dfpo2  30898  wlimss  31022  frrlem7  31034  txpss3v  31155  pprodss4v  31161  relsset  31165  fixssdm  31183  fixssrn  31184  limitssson  31188  funpartss  31221  colinearex  31337  fneer  31518  neibastop1  31524  neibastop2lem  31525  filnetlem2  31544  filnetlem3  31545  knoppcnlem10  31662  bj-tagss  32161  bj-dmtopon  32242  bj-cmnssmnd  32313  bj-ablssgrp  32315  bj-ablsscmn  32317  bj-vecssmod  32320  bj-rrvecssvec  32327  icoreresf  32376  icoreunrn  32383  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimir  32612  broucube  32613  dvasin  32666  dvacos  32667  areacirc  32675  caures  32726  bnd2lem  32760  ismtyres  32777  flddivrng  32968  toycom  33278  dihglblem2N  35601  lcdvbase  35900  mapdunirnN  35957  eldiophb  36338  monotuz  36524  fglmod  36661  pwssplit4  36677  pwfi2f1o  36684  arearect  36820  fvnonrel  36922  rclexi  36941  rtrclex  36943  trclexi  36946  rtrclexi  36947  clcnvlem  36949  cnvrcl0  36951  cnvtrcl0  36952  dfrtrcl5  36955  dfrcl2  36985  comptiunov2i  37017  corclrcl  37018  trclrelexplem  37022  relexpaddss  37029  cotrcltrcl  37036  corcltrcl  37050  cotrclrcl  37053  frege131d  37075  rp-imass  37085  0he  37096  uzmptshftfval  37567  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  rabexgf  38206  uzct  38257  disjf1o  38373  fz1ssfz0  38465  uzfissfz  38483  ssuzfz  38506  limcperiod  38695  sumnnodd  38697  climconstmpt  38725  fnlimfvre  38741  fnlimabslt  38746  cncfshift  38759  cncfperiod  38764  ibliooicc  38863  stoweidlem26  38919  stoweidlem44  38937  stoweidlem50  38943  stoweidlem51  38944  stoweidlem52  38945  stoweidlem57  38950  stoweidlem59  38952  fourierdlem16  39016  fourierdlem19  39019  fourierdlem21  39021  fourierdlem22  39022  fourierdlem42  39042  fourierdlem83  39082  fouriersw  39124  salexct  39228  salexct3  39236  salgencntex  39237  salgensscntex  39238  sge0less  39285  sge0fodjrnlem  39309  sge0isum  39320  ovnsslelem  39450  ovnlerp  39452  ovn0lem  39455  hoidmv1lelem1  39481  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  ovnhoilem1  39491  ovnhoilem2  39492  opnvonmbllem2  39523  ovolval4lem1  39539  ovolval5lem3  39544  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  incsmflem  39628  decsmflem  39652  smflimlem2  39658  smflimlem3  39659  smflim  39663  smfrec  39674  smfmullem4  39679  smfdiv  39682  av-disjxwwlkn  41119  clwwlknclwwlkdifnum  41182  clwwlkssswrd  41218  frgrwopreg1  41487  frgrwopreg2  41488  oddibas  41603  2zlidl  41724  2zrngbas  41726  2zrng0  41728  fldc  41875  fldhmsubc  41876  fldcALTV  41894  fldhmsubcALTV  41895  setrec2lem1  42239