Theorem eqsstri 3935

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

Syntax hints:   = wceq 1543   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  eqsstrri  3936  ssrab2OLD  3994  ssrab3  3995  rabssab  3998  ifssun  4456  opabss  5117  brab2a  5641  relopabiALT  5693  dmopabss  5787  resss  5876  relres  5880  rnin  6010  rnxpss  6035  cnvcnvss  6057  resdmss  6098  resssxp  6133  predss  6167  fnres  6504  f0  6600  nfvres  6753  fvopab4ndm  6847  ffvresb  6941  mptexgf  7038  funiunfv  7061  isoini2  7148  ovssunirn  7249  dmoprabss  7313  mpondm0  7446  elmpocl  7447  exse2  7695  fabexg  7712  frxp  7893  tposssxp  7972  dftpos4  7987  wfrdmss  8061  smores  8089  smores2  8091  iordsmo  8094  swoer  8421  swoord1  8422  swoord2  8423  ecss  8437  ecopovsym  8501  ecopovtrn  8502  ecopover  8503  f1setex  8538  sbthlem7  8762  nnfiOLD  8872  imafiALT  8969  elfiun  9046  marypha1lem  9049  marypha2lem1  9051  hartogslem1  9158  wdomima2g  9202  inf3lem1  9243  tc2  9358  tz9.12lem1  9403  rankuni  9479  rankuniss  9482  rankmapu  9494  hta  9513  r0weon  9626  infxpenlem  9627  ackbij1lem9  9842  ackbij1lem10  9843  ackbij1b  9853  sdom2en01  9916  fin23lem26  9939  fin56  10007  fin1a2lem9  10022  axdc3lem  10064  axdc3lem2  10065  axcclem  10071  imadomg  10148  iundom2g  10154  smobeth  10200  canth4  10261  gruina  10432  grur1a  10433  pinn  10492  niex  10495  ltsopi  10502  ltrelpi  10503  dmaddpi  10504  dmmulpi  10505  enqex  10536  ltrelnq  10540  nqerf  10544  nqerrel  10546  dmrecnq  10582  lterpq  10584  ltrelpr  10612  enrex  10681  ltrelsr  10682  dmaddsr  10699  dmmulsr  10700  ltrelre  10748  axaddf  10759  axmulf  10760  ltrelxr  10894  lerelxr  10896  nn0ssre  12094  nn0sscn  12095  nn0ssz  12198  uzsupss  12536  rpnnen1lem1  12574  rpnnen1lem3  12575  rpnnen1lem5  12577  fz1ssfz0  13208  uzsup  13436  fzfi  13545  swrd00  14209  sqrlem3  14808  cau3  14919  caubnd  14922  limsupgre  15042  rlimpm  15061  rlimclim  15107  isercolllem1  15228  isercolllem2  15229  isercoll  15231  caurcvg  15240  caucvg  15242  iseraltlem2  15246  iseraltlem3  15247  zsum  15282  fsumcvg3  15293  climfsum  15384  ackbijnn  15392  divcnvshft  15419  infcvgaux1i  15421  clim2prod  15452  ntrivcvg  15461  ntrivcvgfvn0  15463  ntrivcvgtail  15464  ntrivcvgmullem  15465  ntrivcvgmul  15466  zprod  15499  dvdszrcl  15820  4sqlem1  16501  4sqlem19  16516  ramub1lem2  16580  structcnvcnv  16706  strleun  16710  fvsetsid  16721  smndex1sgrp  18335  gicer  18680  symgbasfi  18771  mvdco  18837  symgsssg  18859  efglem  19106  efgtf  19112  efgtlen  19116  efginvrel2  19117  efginvrel1  19118  efgsfo  19129  efgredlemg  19132  efgredleme  19133  efgredlemd  19134  efgredlemc  19135  efgredlem  19137  efgred  19138  efgrelexlemb  19140  efgcpbllemb  19145  frgpinv  19154  frgpuplem  19162  frgpupf  19163  frgpup1  19165  frgpnabllem2  19259  gsumval3lem1  19290  gsumval3lem2  19291  gsumval3  19292  lbsextlem3  20197  znf1o  20516  zntoslem  20521  pjpm  20670  mhp0cl  21086  ply1bascl  21124  dmtopon  21820  ordtbas  22089  leordtval2  22109  lecldbas  22116  lmfval  22129  lmbrf  22157  cnconst2  22180  conncompcld  22331  hauspwdom  22398  txuni2  22462  xkouni  22496  xkoccn  22516  txkgen  22549  qtoptop2  22596  kqdisj  22629  hmphtop  22675  hmpher  22681  uzrest  22794  uzfbas  22795  lmflf  22902  tgpconncompeqg  23009  tgpconncomp  23010  ustn0  23118  xmeter  23331  isngp2  23495  xrtgioo  23703  iccntr  23718  xmetdcn  23735  metdcn  23737  metdscn2  23754  icchmeo  23838  cnheiborlem  23851  lmmbrf  24159  iscau4  24176  iscauf  24177  caucfil  24180  lmclimf  24201  volf  24426  uniioombllem3  24482  uniioombllem4  24483  uniioombllem5  24484  volcn  24503  mbfimaopnlem  24552  mbflimsup  24563  i1f1  24587  itg2lcl  24625  itgioo  24713  itgsplitioo  24735  limcflflem  24777  limcflf  24778  limcresi  24782  lhop  24913  dvfsumlem1  24923  dvfsumlem2  24924  dvfsumlem3  24925  dvfsumlem4  24926  dvfsumrlimge0  24927  dvfsumrlim  24928  dvfsumrlim2  24929  dvfsum2  24931  vieta1lem1  25203  vieta1lem2  25204  psercnlem2  25316  psercnlem1  25317  psercn  25318  pserdvlem1  25319  pserdvlem2  25320  pserdv  25321  pserdv2  25322  logcnlem5  25534  dvlog  25539  dvlog2lem  25540  dvlog2  25541  dvcncxp1  25629  dvcnsqrt  25630  cxpcn3lem  25633  cxpcn3  25634  sqrtcn  25636  1cubr  25725  atansssdm  25816  jensen  25871  musum  26073  ppiub  26085  lgsquadlem1  26261  lgsquadlem2  26262  lgsquadlem3  26263  2sqlem7  26305  axtgcgrrflx  26553  axtgcgrid  26554  axtgsegcon  26555  axtg5seg  26556  axtgbtwnid  26557  axtgpasch  26558  axtgcont1  26559  tglng  26637  disjxwwlkn  27997  frgrwopreg2  28402  phnv  28895  htthlem  28998  hlimadd  29274  hlimcaui  29317  hhsscms  29359  occllem  29384  shjshsi  29573  3oalem4  29746  pjfi  29785  dmadjss  29968  nlelshi  30141  nlelchi  30142  hmopidmchi  30232  shatomistici  30442  difxp1ss  30589  difxp2ss  30590  fcoinver  30665  opabssi  30672  mptctf  30772  gsumpart  31034  pmtrcnel2  31078  psgnfzto1stlem  31086  cycpmrn  31129  cyc3genpm  31138  lsmsnorb  31293  cnre2csqima  31575  raddcn  31593  rrhre  31683  esumsnf  31744  sxbrsiga  31969  omssubadd  31979  carsggect  31997  sitmcl  32030  oddpwdc  32033  eulerpartlem1  32046  eulerpartlemt  32050  eulerpartgbij  32051  eulerpartlemmf  32054  eulerpartlemgh  32057  sseqf  32071  ballotlemfmpn  32173  ballotth  32216  signswch  32252  ftc2re  32290  fdvposlt  32291  fdvposle  32293  bnj1146  32484  bnj1292  32508  bnj1293  32509  bnj1145  32686  bnj1177  32699  erdszelem2  32867  kur14lem3  32883  kur14lem6  32886  kur14lem7  32887  kur14lem9  32889  cvmlift2lem12  32989  mpstssv  33214  mstapst  33222  mppspstlem  33246  mppspst  33249  mthmsta  33253  mthmpps  33257  mclsppslem  33258  dfpo2  33441  dmttrcl  33520  rnttrcl  33521  nosupbnd1lem1  33648  nosupbnd2  33656  noinfbnd1lem1  33663  scutf  33743  leftssold  33798  rightssold  33799  txpss3v  33917  pprodss4v  33923  relsset  33927  fixssdm  33945  fixssrn  33946  limitssson  33950  funpartss  33983  colinearex  34099  fneer  34279  neibastop1  34285  neibastop2lem  34286  filnetlem2  34305  filnetlem3  34306  knoppcnlem10  34419  bj-tagss  34907  bj-imdirco  35096  bj-fvsnun2  35162  bj-ablssgrp  35182  bj-ablsscmn  35184  bj-vecssmod  35187  bj-flddrng  35194  icoreresf  35260  icoreunrn  35267  poimirlem29  35543  poimirlem30  35544  poimirlem31  35545  poimir  35547  broucube  35548  dvasin  35598  dvacos  35599  areacirc  35607  caures  35655  bnd2lem  35686  ismtyres  35703  flddivrng  35894  xrnss3v  36239  refrelsredund2  36483  toycom  36724  dihglblem2N  39045  lcdvbase  39344  mapdunirnN  39401  prjspreln0  40156  prjspvs  40157  prjspeclsp  40159  0prjspnrel  40172  dffltz  40174  eldiophb  40282  monotuz  40466  pwssplit4  40617  pwfi2f1o  40624  arearect  40749  fvnonrel  40881  rclexi  40899  rtrclex  40901  trclexi  40904  rtrclexi  40905  clcnvlem  40907  cnvrcl0  40909  cnvtrcl0  40910  dfrtrcl5  40913  dfrcl2  40959  comptiunov2i  40991  corclrcl  40992  trclrelexplem  40996  relexpaddss  41003  cotrcltrcl  41010  corcltrcl  41024  cotrclrcl  41027  frege131d  41049  0he  41067  grumnudlem  41576  uzmptshftfval  41637  binomcxplemdvbinom  41644  binomcxplemdvsum  41646  binomcxplemnotnn0  41647  rabexgf  42240  uzct  42284  disjf1o  42402  dmresss  42447  dmmptssf  42448  mptssid  42457  uzfissfz  42538  ssuzfz  42561  uzssre2  42620  uzublem  42643  uzssz2  42671  uzsscn2  42693  sumnnodd  42846  climconstmpt  42874  fnlimfvre  42890  fnlimabslt  42895  limsupvaluz  42924  limsupubuzlem  42928  limsupubuz  42929  limsupequzmpt2  42934  limsupmnfuzlem  42942  limsupre3uzlem  42951  liminfequzmpt2  43007  ibliooicc  43187  stoweidlem44  43260  stoweidlem50  43266  stoweidlem51  43267  stoweidlem52  43268  stoweidlem57  43273  stoweidlem59  43275  fourierdlem16  43339  fourierdlem19  43342  fourierdlem21  43344  fourierdlem22  43345  fourierdlem42  43365  fourierdlem83  43405  fouriersw  43447  salexct  43548  salexct3  43556  salgencntex  43557  salgensscntex  43558  sge0less  43605  sge0fodjrnlem  43629  sge0isum  43640  ovnsslelem  43773  ovnlerp  43775  ovn0lem  43778  hoidmv1lelem1  43804  hoidmv1lelem3  43806  hoidmvlelem1  43808  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvlelem4  43811  ovnhoilem1  43814  ovnhoilem2  43815  opnvonmbllem2  43846  ovolval4lem1  43862  ovolval5lem3  43867  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  incsmflem  43949  decsmflem  43973  smflimlem2  43979  smflimlem3  43980  smflim  43984  smfrec  43995  smfmullem4  44000  smfdiv  44003  smfsuplem1  44016  smfsuplem3  44018  smfsupxr  44021  smfliminflem  44035  cfsetssfset  44222  fcoreslem2  44230  fcores  44233  oddibas  45040  2zlidl  45165  2zrngbas  45167  2zrng0  45169  fldc  45314  fldhmsubc  45315  fldcALTV  45332  fldhmsubcALTV  45333  ipolub0  45951