Theorem eqsstri 3968

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 231	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqsstrri  3969  3sstr4i  3973  ssrab3  4022  rabssab  4025  ifssun  4484  opabss  5149  brab2a  5724  relopabiALT  5779  dmopabss  5873  rnopabss  5910  resss  5966  relres  5970  rnin  6110  rnxpss  6136  cnvcnvss  6158  resdmss  6199  resssxp  6234  dfpo2  6260  predss  6273  fnres  6625  f0  6721  nfvres  6878  fvopab4ndm  6978  ffvresb  7078  mptexgf  7177  funiunfv  7203  isoini2  7294  ovssunirn  7403  dmoprabss  7471  mpondm0  7607  elmpocl  7608  exse2  7868  fabexgOLD  7890  frxp  8076  tposssxp  8180  dftpos4  8195  smores  8292  smores2  8294  iordsmo  8297  swoer  8675  swoord1  8676  swoord2  8677  ecss  8695  ecopovsym  8766  ecopovtrn  8767  ecopover  8768  f1setex  8804  sbthlem7  9031  imafi  9225  elfiun  9343  marypha1lem  9346  marypha2lem1  9348  hartogslem1  9457  wdomima2g  9501  inf3lem1  9549  dmttrcl  9642  rnttrcl  9643  tc2  9661  frmin  9673  frrlem16  9682  frr1  9683  tz9.12lem1  9711  rankuni  9787  rankuniss  9790  rankmapu  9802  hta  9821  r0weon  9934  infxpenlem  9935  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1b  10160  sdom2en01  10224  fin23lem26  10247  fin56  10315  fin1a2lem9  10330  axdc3lem  10372  axdc3lem2  10373  axcclem  10379  imadomg  10456  iundom2g  10462  smobeth  10509  canth4  10570  gruina  10741  grur1a  10742  pinn  10801  niex  10804  ltsopi  10811  ltrelpi  10812  dmaddpi  10813  dmmulpi  10814  enqex  10845  ltrelnq  10849  nqerf  10853  nqerrel  10855  dmrecnq  10891  lterpq  10893  ltrelpr  10921  enrex  10990  ltrelsr  10991  dmaddsr  11008  dmmulsr  11009  ltrelre  11057  axaddf  11068  axmulf  11069  ltrelxr  11206  lerelxr  11208  nn0ssre  12441  nn0sscn  12442  nn0ssz  12547  uzsupss  12890  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  fz1ssfz0  13577  uzsup  13822  fzfi  13934  swrd00  14607  01sqrexlem3  15206  cau3  15318  caubnd  15321  limsupgre  15443  rlimpm  15462  rlimclim  15508  isercolllem1  15627  isercolllem2  15628  isercoll  15630  caurcvg  15639  caucvg  15641  iseraltlem2  15645  iseraltlem3  15646  zsum  15680  fsumcvg3  15691  climfsum  15783  ackbijnn  15793  divcnvshft  15820  infcvgaux1i  15822  clim2prod  15853  ntrivcvg  15862  ntrivcvgfvn0  15864  ntrivcvgtail  15865  ntrivcvgmullem  15866  ntrivcvgmul  15867  zprod  15902  dvdszrcl  16226  4sqlem1  16919  4sqlem19  16934  ramub1lem2  16998  structcnvcnv  17123  strleun  17127  fvsetsid  17138  smndex1sgrp  18879  gicer  19252  cntzsgrpcl  19309  symgbasfi  19354  mvdco  19420  symgsssg  19442  efglem  19691  efgtf  19697  efgtlen  19701  efginvrel2  19702  efginvrel1  19703  efgsfo  19714  efgredlemg  19717  efgredleme  19718  efgredlemd  19719  efgredlemc  19720  efgredlem  19722  efgred  19723  efgrelexlemb  19725  efgcpbllemb  19730  frgpinv  19739  frgpuplem  19747  frgpupf  19748  frgpup1  19750  frgpnabllem2  19849  gsumval3lem1  19880  gsumval3lem2  19881  gsumval3  19882  fldc  20761  fldhmsubc  20762  lbsextlem3  21158  pzriprnglem10  21470  znf1o  21531  zntoslem  21536  pjpm  21688  mhp0cl  22112  ply1bascl  22167  dmtopon  22888  ordtbas  23157  leordtval2  23177  lecldbas  23184  lmfval  23197  lmbrf  23225  cnconst2  23248  conncompcld  23399  hauspwdom  23466  txuni2  23530  xkouni  23564  xkoccn  23584  txkgen  23617  qtoptop2  23664  kqdisj  23697  hmphtop  23743  hmpher  23749  uzrest  23862  uzfbas  23863  lmflf  23970  tgpconncompeqg  24077  tgpconncomp  24078  ustn0  24186  xmeter  24398  isngp2  24562  xrtgioo  24772  iccntr  24787  xmetdcn  24804  metdcn  24806  metdscn2  24823  cnheiborlem  24921  reparphti  24964  lmmbrf  25229  iscau4  25246  iscauf  25247  caucfil  25250  lmclimf  25271  volf  25496  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  volcn  25573  mbfimaopnlem  25622  mbflimsup  25633  i1f1  25657  itg2lcl  25694  itgioo  25783  itgsplitioo  25805  limcflflem  25847  limcflf  25848  limcresi  25852  lhop  25983  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlimge0  25997  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  vieta1lem1  26276  vieta1lem2  26277  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  pserdv2  26395  logcnlem5  26610  dvlog  26615  dvlog2lem  26616  dvlog2  26617  dvcncxp1  26707  dvcnsqrt  26708  cxpcn3lem  26711  cxpcn3  26712  sqrtcn  26714  1cubr  26806  atansssdm  26897  jensen  26952  musum  27154  ppiub  27167  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  2sqlem7  27387  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbnd1lem1  27687  cutsf  27784  leftssold  27863  rightssold  27864  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  precsexlem8  28206  onssno  28246  nnssn0s  28313  dfnns2  28364  bdaypw2n0bndlem  28455  axtgcgrrflx  28530  axtgcgrid  28531  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgcont1  28536  tglng  28614  disjxwwlkn  29981  frgrwopreg2  30389  phnv  30885  htthlem  30988  hlimadd  31264  hlimcaui  31307  hhsscms  31349  occllem  31374  shjshsi  31563  3oalem4  31736  pjfi  31775  dmadjss  31958  nlelshi  32131  nlelchi  32132  hmopidmchi  32222  shatomistici  32432  difxp1ss  32592  difxp2ss  32593  fcoinver  32674  opabssi  32686  mptctf  32789  ccatws1f1o  33011  gsumpart  33124  pmtrcnel2  33151  psgnfzto1stlem  33161  cycpmrn  33204  cyc3genpm  33213  unitprodclb  33449  lsmsnorb  33451  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  evlextv  33686  vietalem  33723  constrsscn  33884  cnre2csqima  34055  raddcn  34073  zrhcntr  34123  rrhre  34165  esumsnf  34208  sxbrsiga  34434  omssubadd  34444  carsggect  34462  sitmcl  34495  oddpwdc  34498  eulerpartlem1  34511  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpartlemgh  34522  sseqf  34536  ballotlemfmpn  34639  ballotth  34682  signswch  34705  ftc2re  34742  fdvposlt  34743  fdvposle  34745  bnj1146  34933  bnj1292  34957  bnj1293  34958  bnj1145  35135  bnj1177  35148  fineqvnttrclse  35268  tz9.1regs  35278  erdszelem2  35374  kur14lem3  35390  kur14lem6  35393  kur14lem7  35394  kur14lem9  35396  cvmlift2lem12  35496  mpstssv  35721  mstapst  35729  mppspstlem  35753  mppspst  35756  mthmsta  35760  mthmpps  35764  mclsppslem  35765  txpss3v  36058  pprodss4v  36064  relsset  36068  fixssdm  36086  fixssrn  36087  limitssson  36091  funpartss  36126  colinearex  36242  fneer  36535  neibastop1  36541  neibastop2lem  36542  filnetlem2  36561  filnetlem3  36562  ttcuniun  36692  ttcuni  36695  knoppcnlem10  36762  bj-tagss  37287  bj-imdirco  37504  bj-fvsnun2  37570  bj-ablssgrp  37590  bj-ablsscmn  37592  bj-vecssmod  37595  bj-fldssdrng  37602  icoreresf  37668  icoreunrn  37675  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimir  37974  broucube  37975  dvasin  38025  dvacos  38026  areacirc  38034  caures  38081  bnd2lem  38112  ismtyres  38129  flddivrng  38320  xrnss3v  38702  refrelsredund2  39038  toycom  39419  dihglblem2N  41740  lcdvbase  42039  mapdunirnN  42096  aks6d1c1p1rcl  42547  redvmptabs  42792  readvrec  42794  prjspreln0  43042  prjspvs  43043  prjspeclsp  43045  0prjspnrel  43060  dffltz  43067  eldiophb  43189  monotuz  43369  pwssplit4  43517  pwfi2f1o  43524  arearect  43643  cantnfresb  43752  omabs2  43760  fvnonrel  44024  rclexi  44042  rtrclex  44044  trclexi  44047  rtrclexi  44048  clcnvlem  44050  cnvrcl0  44052  cnvtrcl0  44053  dfrtrcl5  44056  dfrcl2  44101  comptiunov2i  44133  corclrcl  44134  trclrelexplem  44138  relexpaddss  44145  cotrcltrcl  44152  corcltrcl  44166  cotrclrcl  44169  frege131d  44191  0he  44209  grumnudlem  44712  uzmptshftfval  44773  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  modelaxreplem2  45406  rabexgf  45455  uzct  45494  disjf1o  45621  dmmptssf  45661  mptssid  45670  uzfissfz  45756  ssuzfz  45779  uzssre2  45835  uzublem  45858  uzssz2  45884  uzsscn2  45905  sumnnodd  46060  climconstmpt  46086  fnlimfvre  46102  fnlimabslt  46107  limsupvaluz  46136  limsupubuzlem  46140  limsupubuz  46141  limsupequzmpt2  46146  limsupmnfuzlem  46154  limsupre3uzlem  46163  liminfequzmpt2  46219  ibliooicc  46399  stoweidlem44  46472  stoweidlem50  46478  stoweidlem51  46479  stoweidlem52  46480  stoweidlem57  46485  stoweidlem59  46487  fourierdlem16  46551  fourierdlem19  46554  fourierdlem21  46556  fourierdlem22  46557  fourierdlem42  46577  fourierdlem83  46617  fouriersw  46659  salexct  46762  salexct3  46770  salgencntex  46771  salgensscntex  46772  sge0less  46820  sge0fodjrnlem  46844  sge0isum  46855  ovnlerp  46990  ovn0lem  46993  hoidmv1lelem1  47019  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  ovnhoilem1  47029  ovnhoilem2  47030  opnvonmbllem2  47061  ovolval4lem1  47077  ovolval5lem3  47082  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  incsmflem  47169  decsmflem  47194  smflimlem2  47200  smflimlem3  47201  smflim  47205  smfrec  47217  smfmullem4  47222  smfdiv  47225  smfsuplem1  47239  smfsuplem3  47241  smfsupxr  47244  smfliminflem  47258  cfsetssfset  47504  fcoreslem2  47512  fcores  47515  gricrel  48395  clnbgrisubgrgrim  48408  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  isubgr3stgrlem8  48449  isubgr3stgr  48451  grlimgrtrilem2  48478  grlicrel  48482  oddibas  48649  2zlidl  48716  2zrngbas  48718  2zrng0  48720  fldcALTV  48808  fldhmsubcALTV  48809  dmtposss  49351  tposres3  49356  ipolub0  49467  imaidfu  49585