Theorem eqsstri 4030

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

Syntax hints:   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  eqsstrri  4031  3sstr4i  4035  ssrab3  4082  rabssab  4085  ifssun  4543  opabss  5207  brab2a  5779  relopabiALT  5833  dmopabss  5929  rnopabss  5966  resss  6019  relres  6023  rnin  6166  rnxpss  6192  cnvcnvss  6214  resdmss  6255  resssxp  6290  dfpo2  6316  predss  6329  fnres  6695  f0  6789  nfvres  6947  fvopab4ndm  7046  ffvresb  7145  mptexgf  7242  funiunfv  7268  isoini2  7359  ovssunirn  7467  dmoprabss  7537  mpondm0  7673  elmpocl  7674  exse2  7939  fabexgOLD  7961  frxp  8151  tposssxp  8255  dftpos4  8270  wfrdmssOLD  8355  smores  8392  smores2  8394  iordsmo  8397  swoer  8776  swoord1  8777  swoord2  8778  ecss  8793  ecopovsym  8859  ecopovtrn  8860  ecopover  8861  f1setex  8897  sbthlem7  9129  imafi  9353  elfiun  9470  marypha1lem  9473  marypha2lem1  9475  hartogslem1  9582  wdomima2g  9626  inf3lem1  9668  dmttrcl  9761  rnttrcl  9762  tc2  9782  frmin  9789  frrlem16  9798  frr1  9799  tz9.12lem1  9827  rankuni  9903  rankuniss  9906  rankmapu  9918  hta  9937  r0weon  10052  infxpenlem  10053  ackbij1lem9  10267  ackbij1lem10  10268  ackbij1b  10278  sdom2en01  10342  fin23lem26  10365  fin56  10433  fin1a2lem9  10448  axdc3lem  10490  axdc3lem2  10491  axcclem  10497  imadomg  10574  iundom2g  10580  smobeth  10626  canth4  10687  gruina  10858  grur1a  10859  pinn  10918  niex  10921  ltsopi  10928  ltrelpi  10929  dmaddpi  10930  dmmulpi  10931  enqex  10962  ltrelnq  10966  nqerf  10970  nqerrel  10972  dmrecnq  11008  lterpq  11010  ltrelpr  11038  enrex  11107  ltrelsr  11108  dmaddsr  11125  dmmulsr  11126  ltrelre  11174  axaddf  11185  axmulf  11186  ltrelxr  11322  lerelxr  11324  nn0ssre  12530  nn0sscn  12531  nn0ssz  12636  uzsupss  12982  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  fz1ssfz0  13663  uzsup  13903  fzfi  14013  swrd00  14682  01sqrexlem3  15283  cau3  15394  caubnd  15397  limsupgre  15517  rlimpm  15536  rlimclim  15582  isercolllem1  15701  isercolllem2  15702  isercoll  15704  caurcvg  15713  caucvg  15715  iseraltlem2  15719  iseraltlem3  15720  zsum  15754  fsumcvg3  15765  climfsum  15856  ackbijnn  15864  divcnvshft  15891  infcvgaux1i  15893  clim2prod  15924  ntrivcvg  15933  ntrivcvgfvn0  15935  ntrivcvgtail  15936  ntrivcvgmullem  15937  ntrivcvgmul  15938  zprod  15973  dvdszrcl  16295  4sqlem1  16986  4sqlem19  17001  ramub1lem2  17065  structcnvcnv  17190  strleun  17194  fvsetsid  17205  smndex1sgrp  18921  gicer  19295  cntzsgrpcl  19352  symgbasfi  19396  mvdco  19463  symgsssg  19485  efglem  19734  efgtf  19740  efgtlen  19744  efginvrel2  19745  efginvrel1  19746  efgsfo  19757  efgredlemg  19760  efgredleme  19761  efgredlemd  19762  efgredlemc  19763  efgredlem  19765  efgred  19766  efgrelexlemb  19768  efgcpbllemb  19773  frgpinv  19782  frgpuplem  19790  frgpupf  19791  frgpup1  19793  frgpnabllem2  19892  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  fldc  20785  fldhmsubc  20786  lbsextlem3  21162  pzriprnglem10  21501  znf1o  21570  zntoslem  21575  pjpm  21728  mhp0cl  22150  ply1bascl  22205  dmtopon  22929  ordtbas  23200  leordtval2  23220  lecldbas  23227  lmfval  23240  lmbrf  23268  cnconst2  23291  conncompcld  23442  hauspwdom  23509  txuni2  23573  xkouni  23607  xkoccn  23627  txkgen  23660  qtoptop2  23707  kqdisj  23740  hmphtop  23786  hmpher  23792  uzrest  23905  uzfbas  23906  lmflf  24013  tgpconncompeqg  24120  tgpconncomp  24121  ustn0  24229  xmeter  24443  isngp2  24610  xrtgioo  24828  iccntr  24843  xmetdcn  24860  metdcn  24862  metdscn2  24879  icchmeoOLD  24972  cnheiborlem  24986  reparphti  25029  lmmbrf  25296  iscau4  25313  iscauf  25314  caucfil  25317  lmclimf  25338  volf  25564  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  volcn  25641  mbfimaopnlem  25690  mbflimsup  25701  i1f1  25725  itg2lcl  25762  itgioo  25851  itgsplitioo  25873  limcflflem  25915  limcflf  25916  limcresi  25920  lhop  26055  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlimge0  26071  dvfsumrlim  26072  dvfsumrlim2  26073  dvfsum2  26075  vieta1lem1  26352  vieta1lem2  26353  psercnlem2  26468  psercnlem1  26469  psercn  26470  pserdvlem1  26471  pserdvlem2  26472  pserdv  26473  pserdv2  26474  logcnlem5  26688  dvlog  26693  dvlog2lem  26694  dvlog2  26695  dvcncxp1  26785  dvcnsqrt  26786  cxpcn3lem  26790  cxpcn3  26791  sqrtcn  26793  1cubr  26885  atansssdm  26976  jensen  27032  musum  27234  ppiub  27248  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  2sqlem7  27468  nosupbnd1lem1  27753  nosupbnd2  27761  noinfbnd1lem1  27768  scutf  27857  leftssold  27917  rightssold  27918  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  precsexlem8  28238  onssno  28277  nnssn0s  28326  dfnns2  28362  axtgcgrrflx  28470  axtgcgrid  28471  axtgsegcon  28472  axtg5seg  28473  axtgbtwnid  28474  axtgpasch  28475  axtgcont1  28476  tglng  28554  disjxwwlkn  29933  frgrwopreg2  30338  phnv  30833  htthlem  30936  hlimadd  31212  hlimcaui  31255  hhsscms  31297  occllem  31322  shjshsi  31511  3oalem4  31684  pjfi  31723  dmadjss  31906  nlelshi  32079  nlelchi  32080  hmopidmchi  32170  shatomistici  32380  difxp1ss  32541  difxp2ss  32542  fcoinver  32617  opabssi  32625  mptctf  32729  ccatws1f1o  32936  gsumpart  33060  pmtrcnel2  33110  psgnfzto1stlem  33120  cycpmrn  33163  cyc3genpm  33172  unitprodclb  33417  lsmsnorb  33419  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  constrsscn  33781  cnre2csqima  33910  raddcn  33928  zrhcntr  33980  rrhre  34022  esumsnf  34065  sxbrsiga  34292  omssubadd  34302  carsggect  34320  sitmcl  34353  oddpwdc  34356  eulerpartlem1  34369  eulerpartlemt  34373  eulerpartgbij  34374  eulerpartlemmf  34377  eulerpartlemgh  34380  sseqf  34394  ballotlemfmpn  34497  ballotth  34540  signswch  34576  ftc2re  34613  fdvposlt  34614  fdvposle  34616  bnj1146  34805  bnj1292  34829  bnj1293  34830  bnj1145  35007  bnj1177  35020  erdszelem2  35197  kur14lem3  35213  kur14lem6  35216  kur14lem7  35217  kur14lem9  35219  cvmlift2lem12  35319  mpstssv  35544  mstapst  35552  mppspstlem  35576  mppspst  35579  mthmsta  35583  mthmpps  35587  mclsppslem  35588  txpss3v  35879  pprodss4v  35885  relsset  35889  fixssdm  35907  fixssrn  35908  limitssson  35912  funpartss  35945  colinearex  36061  fneer  36354  neibastop1  36360  neibastop2lem  36361  filnetlem2  36380  filnetlem3  36381  knoppcnlem10  36503  bj-tagss  36981  bj-imdirco  37191  bj-fvsnun2  37257  bj-ablssgrp  37277  bj-ablsscmn  37279  bj-vecssmod  37282  bj-fldssdrng  37289  icoreresf  37353  icoreunrn  37360  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimir  37660  broucube  37661  dvasin  37711  dvacos  37712  areacirc  37720  caures  37767  bnd2lem  37798  ismtyres  37815  flddivrng  38006  xrnss3v  38373  refrelsredund2  38634  toycom  38974  dihglblem2N  41296  lcdvbase  41595  mapdunirnN  41652  aks6d1c1p1rcl  42109  redvmptabs  42390  readvrec  42392  prjspreln0  42619  prjspvs  42620  prjspeclsp  42622  0prjspnrel  42637  dffltz  42644  eldiophb  42768  monotuz  42953  pwssplit4  43101  pwfi2f1o  43108  arearect  43227  cantnfresb  43337  omabs2  43345  fvnonrel  43610  rclexi  43628  rtrclex  43630  trclexi  43633  rtrclexi  43634  clcnvlem  43636  cnvrcl0  43638  cnvtrcl0  43639  dfrtrcl5  43642  dfrcl2  43687  comptiunov2i  43719  corclrcl  43720  trclrelexplem  43724  relexpaddss  43731  cotrcltrcl  43738  corcltrcl  43752  cotrclrcl  43755  frege131d  43777  0he  43795  grumnudlem  44304  uzmptshftfval  44365  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  modelaxreplem2  44996  rabexgf  45029  uzct  45068  disjf1o  45196  dmmptssf  45237  mptssid  45247  uzfissfz  45337  ssuzfz  45360  uzssre2  45418  uzublem  45441  uzssz2  45467  uzsscn2  45488  sumnnodd  45645  climconstmpt  45673  fnlimfvre  45689  fnlimabslt  45694  limsupvaluz  45723  limsupubuzlem  45727  limsupubuz  45728  limsupequzmpt2  45733  limsupmnfuzlem  45741  limsupre3uzlem  45750  liminfequzmpt2  45806  ibliooicc  45986  stoweidlem44  46059  stoweidlem50  46065  stoweidlem51  46066  stoweidlem52  46067  stoweidlem57  46072  stoweidlem59  46074  fourierdlem16  46138  fourierdlem19  46141  fourierdlem21  46143  fourierdlem22  46144  fourierdlem42  46164  fourierdlem83  46204  fouriersw  46246  salexct  46349  salexct3  46357  salgencntex  46358  salgensscntex  46359  sge0less  46407  sge0fodjrnlem  46431  sge0isum  46442  ovnlerp  46577  ovn0lem  46580  hoidmv1lelem1  46606  hoidmv1lelem3  46608  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  ovnhoilem1  46616  ovnhoilem2  46617  opnvonmbllem2  46648  ovolval4lem1  46664  ovolval5lem3  46669  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  incsmflem  46756  decsmflem  46781  smflimlem2  46787  smflimlem3  46788  smflim  46792  smfrec  46804  smfmullem4  46809  smfdiv  46812  smfsuplem1  46826  smfsuplem3  46828  smfsupxr  46831  smfliminflem  46845  cfsetssfset  47068  fcoreslem2  47076  fcores  47079  gricrel  47888  clnbgrisubgrgrim  47900  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  isubgr3stgrlem8  47940  isubgr3stgr  47942  grlimgrtrilem2  47962  grlicrel  47966  oddibas  48089  2zlidl  48156  2zrngbas  48158  2zrng0  48160  fldcALTV  48248  fldhmsubcALTV  48249  dmtposss  48776  tposres3  48781  ipolub0  48881