Theorem eqsstri 3956

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

Syntax hints:   = wceq 1539   ⊆ wss 3888

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  eqsstrri  3957  ssrab2OLD  4015  ssrab3  4016  rabssab  4019  ifssun  4477  opabss  5139  brab2a  5681  relopabiALT  5735  dmopabss  5830  resss  5919  relres  5923  rnin  6055  rnxpss  6080  cnvcnvss  6102  resdmss  6143  resssxp  6177  dfpo2  6203  predss  6214  fnres  6568  f0  6664  nfvres  6819  fvopab4ndm  6913  ffvresb  7007  mptexgf  7107  funiunfv  7130  isoini2  7219  ovssunirn  7320  dmoprabss  7386  mpondm0  7519  elmpocl  7520  exse2  7773  fabexg  7790  frxp  7976  tposssxp  8055  dftpos4  8070  wfrdmssOLD  8155  smores  8192  smores2  8194  iordsmo  8197  swoer  8537  swoord1  8538  swoord2  8539  ecss  8553  ecopovsym  8617  ecopovtrn  8618  ecopover  8619  f1setex  8654  sbthlem7  8885  nnfiOLD  9024  imafiALT  9121  elfiun  9198  marypha1lem  9201  marypha2lem1  9203  hartogslem1  9310  wdomima2g  9354  inf3lem1  9395  dmttrcl  9488  rnttrcl  9489  tc2  9509  frmin  9516  frrlem16  9525  frr1  9526  tz9.12lem1  9554  rankuni  9630  rankuniss  9633  rankmapu  9645  hta  9664  r0weon  9777  infxpenlem  9778  ackbij1lem9  9993  ackbij1lem10  9994  ackbij1b  10004  sdom2en01  10067  fin23lem26  10090  fin56  10158  fin1a2lem9  10173  axdc3lem  10215  axdc3lem2  10216  axcclem  10222  imadomg  10299  iundom2g  10305  smobeth  10351  canth4  10412  gruina  10583  grur1a  10584  pinn  10643  niex  10646  ltsopi  10653  ltrelpi  10654  dmaddpi  10655  dmmulpi  10656  enqex  10687  ltrelnq  10691  nqerf  10695  nqerrel  10697  dmrecnq  10733  lterpq  10735  ltrelpr  10763  enrex  10832  ltrelsr  10833  dmaddsr  10850  dmmulsr  10851  ltrelre  10899  axaddf  10910  axmulf  10911  ltrelxr  11045  lerelxr  11047  nn0ssre  12246  nn0sscn  12247  nn0ssz  12350  uzsupss  12689  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  fz1ssfz0  13361  uzsup  13592  fzfi  13701  swrd00  14366  sqrlem3  14965  cau3  15076  caubnd  15079  limsupgre  15199  rlimpm  15218  rlimclim  15264  isercolllem1  15385  isercolllem2  15386  isercoll  15388  caurcvg  15397  caucvg  15399  iseraltlem2  15403  iseraltlem3  15404  zsum  15439  fsumcvg3  15450  climfsum  15541  ackbijnn  15549  divcnvshft  15576  infcvgaux1i  15578  clim2prod  15609  ntrivcvg  15618  ntrivcvgfvn0  15620  ntrivcvgtail  15621  ntrivcvgmullem  15622  ntrivcvgmul  15623  zprod  15656  dvdszrcl  15977  4sqlem1  16658  4sqlem19  16673  ramub1lem2  16737  structcnvcnv  16863  strleun  16867  fvsetsid  16878  smndex1sgrp  18556  gicer  18901  symgbasfi  18995  mvdco  19062  symgsssg  19084  efglem  19331  efgtf  19337  efgtlen  19341  efginvrel2  19342  efginvrel1  19343  efgsfo  19354  efgredlemg  19357  efgredleme  19358  efgredlemd  19359  efgredlemc  19360  efgredlem  19362  efgred  19363  efgrelexlemb  19365  efgcpbllemb  19370  frgpinv  19379  frgpuplem  19387  frgpupf  19388  frgpup1  19390  frgpnabllem2  19484  gsumval3lem1  19515  gsumval3lem2  19516  gsumval3  19517  lbsextlem3  20431  znf1o  20768  zntoslem  20773  pjpm  20924  mhp0cl  21345  ply1bascl  21383  dmtopon  22081  ordtbas  22352  leordtval2  22372  lecldbas  22379  lmfval  22392  lmbrf  22420  cnconst2  22443  conncompcld  22594  hauspwdom  22661  txuni2  22725  xkouni  22759  xkoccn  22779  txkgen  22812  qtoptop2  22859  kqdisj  22892  hmphtop  22938  hmpher  22944  uzrest  23057  uzfbas  23058  lmflf  23165  tgpconncompeqg  23272  tgpconncomp  23273  ustn0  23381  xmeter  23595  isngp2  23762  xrtgioo  23978  iccntr  23993  xmetdcn  24010  metdcn  24012  metdscn2  24029  icchmeo  24113  cnheiborlem  24126  lmmbrf  24435  iscau4  24452  iscauf  24453  caucfil  24456  lmclimf  24477  volf  24702  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  volcn  24779  mbfimaopnlem  24828  mbflimsup  24839  i1f1  24863  itg2lcl  24901  itgioo  24989  itgsplitioo  25011  limcflflem  25053  limcflf  25054  limcresi  25058  lhop  25189  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsumrlimge0  25203  dvfsumrlim  25204  dvfsumrlim2  25205  dvfsum2  25207  vieta1lem1  25479  vieta1lem2  25480  psercnlem2  25592  psercnlem1  25593  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  pserdv  25597  pserdv2  25598  logcnlem5  25810  dvlog  25815  dvlog2lem  25816  dvlog2  25817  dvcncxp1  25905  dvcnsqrt  25906  cxpcn3lem  25909  cxpcn3  25910  sqrtcn  25912  1cubr  26001  atansssdm  26092  jensen  26147  musum  26349  ppiub  26361  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  2sqlem7  26581  axtgcgrrflx  26832  axtgcgrid  26833  axtgsegcon  26834  axtg5seg  26835  axtgbtwnid  26836  axtgpasch  26837  axtgcont1  26838  tglng  26916  disjxwwlkn  28287  frgrwopreg2  28692  phnv  29185  htthlem  29288  hlimadd  29564  hlimcaui  29607  hhsscms  29649  occllem  29674  shjshsi  29863  3oalem4  30036  pjfi  30075  dmadjss  30258  nlelshi  30431  nlelchi  30432  hmopidmchi  30522  shatomistici  30732  difxp1ss  30879  difxp2ss  30880  fcoinver  30955  opabssi  30962  mptctf  31061  gsumpart  31324  pmtrcnel2  31368  psgnfzto1stlem  31376  cycpmrn  31419  cyc3genpm  31428  lsmsnorb  31588  cnre2csqima  31870  raddcn  31888  rrhre  31980  esumsnf  32041  sxbrsiga  32266  omssubadd  32276  carsggect  32294  sitmcl  32327  oddpwdc  32330  eulerpartlem1  32343  eulerpartlemt  32347  eulerpartgbij  32348  eulerpartlemmf  32351  eulerpartlemgh  32354  sseqf  32368  ballotlemfmpn  32470  ballotth  32513  signswch  32549  ftc2re  32587  fdvposlt  32588  fdvposle  32590  bnj1146  32780  bnj1292  32804  bnj1293  32805  bnj1145  32982  bnj1177  32995  erdszelem2  33163  kur14lem3  33179  kur14lem6  33182  kur14lem7  33183  kur14lem9  33185  cvmlift2lem12  33285  mpstssv  33510  mstapst  33518  mppspstlem  33542  mppspst  33545  mthmsta  33549  mthmpps  33553  mclsppslem  33554  nosupbnd1lem1  33920  nosupbnd2  33928  noinfbnd1lem1  33935  scutf  34015  leftssold  34070  rightssold  34071  txpss3v  34189  pprodss4v  34195  relsset  34199  fixssdm  34217  fixssrn  34218  limitssson  34222  funpartss  34255  colinearex  34371  fneer  34551  neibastop1  34557  neibastop2lem  34558  filnetlem2  34577  filnetlem3  34578  knoppcnlem10  34691  bj-tagss  35179  bj-imdirco  35370  bj-fvsnun2  35436  bj-ablssgrp  35456  bj-ablsscmn  35458  bj-vecssmod  35461  bj-fldssdrng  35468  icoreresf  35532  icoreunrn  35539  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimir  35819  broucube  35820  dvasin  35870  dvacos  35871  areacirc  35879  caures  35927  bnd2lem  35958  ismtyres  35975  flddivrng  36166  xrnss3v  36509  refrelsredund2  36753  toycom  36994  dihglblem2N  39315  lcdvbase  39614  mapdunirnN  39671  prjspreln0  40455  prjspvs  40456  prjspeclsp  40458  0prjspnrel  40471  dffltz  40478  eldiophb  40586  monotuz  40770  pwssplit4  40921  pwfi2f1o  40928  arearect  41053  fvnonrel  41212  rclexi  41230  rtrclex  41232  trclexi  41235  rtrclexi  41236  clcnvlem  41238  cnvrcl0  41240  cnvtrcl0  41241  dfrtrcl5  41244  dfrcl2  41289  comptiunov2i  41321  corclrcl  41322  trclrelexplem  41326  relexpaddss  41333  cotrcltrcl  41340  corcltrcl  41354  cotrclrcl  41357  frege131d  41379  0he  41397  grumnudlem  41910  uzmptshftfval  41971  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  rabexgf  42574  uzct  42618  disjf1o  42736  dmresss  42781  dmmptssf  42782  mptssid  42792  uzfissfz  42872  ssuzfz  42895  uzssre2  42954  uzublem  42977  uzssz2  43003  uzsscn2  43025  sumnnodd  43178  climconstmpt  43206  fnlimfvre  43222  fnlimabslt  43227  limsupvaluz  43256  limsupubuzlem  43260  limsupubuz  43261  limsupequzmpt2  43266  limsupmnfuzlem  43274  limsupre3uzlem  43283  liminfequzmpt2  43339  ibliooicc  43519  stoweidlem44  43592  stoweidlem50  43598  stoweidlem51  43599  stoweidlem52  43600  stoweidlem57  43605  stoweidlem59  43607  fourierdlem16  43671  fourierdlem19  43674  fourierdlem21  43676  fourierdlem22  43677  fourierdlem42  43697  fourierdlem83  43737  fouriersw  43779  salexct  43880  salexct3  43888  salgencntex  43889  salgensscntex  43890  sge0less  43937  sge0fodjrnlem  43961  sge0isum  43972  ovnsslelem  44105  ovnlerp  44107  ovn0lem  44110  hoidmv1lelem1  44136  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  ovnhoilem1  44146  ovnhoilem2  44147  opnvonmbllem2  44178  ovolval4lem1  44194  ovolval5lem3  44199  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  incsmflem  44286  decsmflem  44311  smflimlem2  44317  smflimlem3  44318  smflim  44322  smfrec  44334  smfmullem4  44339  smfdiv  44342  smfsuplem1  44355  smfsuplem3  44357  smfsupxr  44360  smfliminflem  44374  cfsetssfset  44561  fcoreslem2  44569  fcores  44572  oddibas  45378  2zlidl  45503  2zrngbas  45505  2zrng0  45507  fldc  45652  fldhmsubc  45653  fldcALTV  45670  fldhmsubcALTV  45671  ipolub0  46289