Theorem eqsstri 4043

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqsstrri  4044  ssrab3  4105  rabssab  4108  ifssun  4565  opabss  5230  brab2a  5793  relopabiALT  5847  dmopabss  5943  resss  6031  relres  6035  rnin  6178  rnxpss  6203  cnvcnvss  6225  resdmss  6266  resssxp  6301  dfpo2  6327  predss  6340  fnres  6707  f0  6802  nfvres  6961  fvopab4ndm  7059  ffvresb  7159  mptexgf  7259  funiunfv  7285  isoini2  7375  ovssunirn  7484  dmoprabss  7553  mpondm0  7690  elmpocl  7691  exse2  7957  fabexgOLD  7977  frxp  8167  tposssxp  8271  dftpos4  8286  wfrdmssOLD  8371  smores  8408  smores2  8410  iordsmo  8413  swoer  8794  swoord1  8795  swoord2  8796  ecss  8811  ecopovsym  8877  ecopovtrn  8878  ecopover  8879  f1setex  8915  sbthlem7  9155  nnfiOLD  9295  imafi  9381  elfiun  9499  marypha1lem  9502  marypha2lem1  9504  hartogslem1  9611  wdomima2g  9655  inf3lem1  9697  dmttrcl  9790  rnttrcl  9791  tc2  9811  frmin  9818  frrlem16  9827  frr1  9828  tz9.12lem1  9856  rankuni  9932  rankuniss  9935  rankmapu  9947  hta  9966  r0weon  10081  infxpenlem  10082  ackbij1lem9  10296  ackbij1lem10  10297  ackbij1b  10307  sdom2en01  10371  fin23lem26  10394  fin56  10462  fin1a2lem9  10477  axdc3lem  10519  axdc3lem2  10520  axcclem  10526  imadomg  10603  iundom2g  10609  smobeth  10655  canth4  10716  gruina  10887  grur1a  10888  pinn  10947  niex  10950  ltsopi  10957  ltrelpi  10958  dmaddpi  10959  dmmulpi  10960  enqex  10991  ltrelnq  10995  nqerf  10999  nqerrel  11001  dmrecnq  11037  lterpq  11039  ltrelpr  11067  enrex  11136  ltrelsr  11137  dmaddsr  11154  dmmulsr  11155  ltrelre  11203  axaddf  11214  axmulf  11215  ltrelxr  11351  lerelxr  11353  nn0ssre  12557  nn0sscn  12558  nn0ssz  12662  uzsupss  13005  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  fz1ssfz0  13680  uzsup  13914  fzfi  14023  swrd00  14692  01sqrexlem3  15293  cau3  15404  caubnd  15407  limsupgre  15527  rlimpm  15546  rlimclim  15592  isercolllem1  15713  isercolllem2  15714  isercoll  15716  caurcvg  15725  caucvg  15727  iseraltlem2  15731  iseraltlem3  15732  zsum  15766  fsumcvg3  15777  climfsum  15868  ackbijnn  15876  divcnvshft  15903  infcvgaux1i  15905  clim2prod  15936  ntrivcvg  15945  ntrivcvgfvn0  15947  ntrivcvgtail  15948  ntrivcvgmullem  15949  ntrivcvgmul  15950  zprod  15985  dvdszrcl  16307  4sqlem1  16995  4sqlem19  17010  ramub1lem2  17074  structcnvcnv  17200  strleun  17204  fvsetsid  17215  smndex1sgrp  18943  gicer  19317  cntzsgrpcl  19374  symgbasfi  19420  mvdco  19487  symgsssg  19509  efglem  19758  efgtf  19764  efgtlen  19768  efginvrel2  19769  efginvrel1  19770  efgsfo  19781  efgredlemg  19784  efgredleme  19785  efgredlemd  19786  efgredlemc  19787  efgredlem  19789  efgred  19790  efgrelexlemb  19792  efgcpbllemb  19797  frgpinv  19806  frgpuplem  19814  frgpupf  19815  frgpup1  19817  frgpnabllem2  19916  gsumval3lem1  19947  gsumval3lem2  19948  gsumval3  19949  fldc  20807  fldhmsubc  20808  lbsextlem3  21185  pzriprnglem10  21524  znf1o  21593  zntoslem  21598  pjpm  21751  mhp0cl  22173  ply1bascl  22226  dmtopon  22950  ordtbas  23221  leordtval2  23241  lecldbas  23248  lmfval  23261  lmbrf  23289  cnconst2  23312  conncompcld  23463  hauspwdom  23530  txuni2  23594  xkouni  23628  xkoccn  23648  txkgen  23681  qtoptop2  23728  kqdisj  23761  hmphtop  23807  hmpher  23813  uzrest  23926  uzfbas  23927  lmflf  24034  tgpconncompeqg  24141  tgpconncomp  24142  ustn0  24250  xmeter  24464  isngp2  24631  xrtgioo  24847  iccntr  24862  xmetdcn  24879  metdcn  24881  metdscn2  24898  icchmeoOLD  24991  cnheiborlem  25005  reparphti  25048  lmmbrf  25315  iscau4  25332  iscauf  25333  caucfil  25336  lmclimf  25357  volf  25583  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  volcn  25660  mbfimaopnlem  25709  mbflimsup  25720  i1f1  25744  itg2lcl  25782  itgioo  25871  itgsplitioo  25893  limcflflem  25935  limcflf  25936  limcresi  25940  lhop  26075  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlimge0  26091  dvfsumrlim  26092  dvfsumrlim2  26093  dvfsum2  26095  vieta1lem1  26370  vieta1lem2  26371  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  pserdv  26491  pserdv2  26492  logcnlem5  26706  dvlog  26711  dvlog2lem  26712  dvlog2  26713  dvcncxp1  26803  dvcnsqrt  26804  cxpcn3lem  26808  cxpcn3  26809  sqrtcn  26811  1cubr  26903  atansssdm  26994  jensen  27050  musum  27252  ppiub  27266  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  2sqlem7  27486  nosupbnd1lem1  27771  nosupbnd2  27779  noinfbnd1lem1  27786  scutf  27875  leftssold  27935  rightssold  27936  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  precsexlem8  28256  onssno  28295  nnssn0s  28344  dfnns2  28380  axtgcgrrflx  28488  axtgcgrid  28489  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgcont1  28494  tglng  28572  disjxwwlkn  29946  frgrwopreg2  30351  phnv  30846  htthlem  30949  hlimadd  31225  hlimcaui  31268  hhsscms  31310  occllem  31335  shjshsi  31524  3oalem4  31697  pjfi  31736  dmadjss  31919  nlelshi  32092  nlelchi  32093  hmopidmchi  32183  shatomistici  32393  difxp1ss  32552  difxp2ss  32553  fcoinver  32626  opabssi  32635  mptctf  32731  ccatws1f1o  32918  gsumpart  33038  pmtrcnel2  33083  psgnfzto1stlem  33093  cycpmrn  33136  cyc3genpm  33145  unitprodclb  33382  lsmsnorb  33384  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  constrsscn  33730  cnre2csqima  33857  raddcn  33875  rrhre  33967  esumsnf  34028  sxbrsiga  34255  omssubadd  34265  carsggect  34283  sitmcl  34316  oddpwdc  34319  eulerpartlem1  34332  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpartlemgh  34343  sseqf  34357  ballotlemfmpn  34459  ballotth  34502  signswch  34538  ftc2re  34575  fdvposlt  34576  fdvposle  34578  bnj1146  34767  bnj1292  34791  bnj1293  34792  bnj1145  34969  bnj1177  34982  erdszelem2  35160  kur14lem3  35176  kur14lem6  35179  kur14lem7  35180  kur14lem9  35182  cvmlift2lem12  35282  mpstssv  35507  mstapst  35515  mppspstlem  35539  mppspst  35542  mthmsta  35546  mthmpps  35550  mclsppslem  35551  txpss3v  35842  pprodss4v  35848  relsset  35852  fixssdm  35870  fixssrn  35871  limitssson  35875  funpartss  35908  colinearex  36024  fneer  36319  neibastop1  36325  neibastop2lem  36326  filnetlem2  36345  filnetlem3  36346  knoppcnlem10  36468  bj-tagss  36946  bj-imdirco  37156  bj-fvsnun2  37222  bj-ablssgrp  37242  bj-ablsscmn  37244  bj-vecssmod  37247  bj-fldssdrng  37254  icoreresf  37318  icoreunrn  37325  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimir  37613  broucube  37614  dvasin  37664  dvacos  37665  areacirc  37673  caures  37720  bnd2lem  37751  ismtyres  37768  flddivrng  37959  xrnss3v  38328  refrelsredund2  38589  toycom  38929  dihglblem2N  41251  lcdvbase  41550  mapdunirnN  41607  aks6d1c1p1rcl  42065  prjspreln0  42564  prjspvs  42565  prjspeclsp  42567  0prjspnrel  42582  dffltz  42589  eldiophb  42713  monotuz  42898  pwssplit4  43046  pwfi2f1o  43053  arearect  43176  cantnfresb  43286  omabs2  43294  fvnonrel  43559  rclexi  43577  rtrclex  43579  trclexi  43582  rtrclexi  43583  clcnvlem  43585  cnvrcl0  43587  cnvtrcl0  43588  dfrtrcl5  43591  dfrcl2  43636  comptiunov2i  43668  corclrcl  43669  trclrelexplem  43673  relexpaddss  43680  cotrcltrcl  43687  corcltrcl  43701  cotrclrcl  43704  frege131d  43726  0he  43744  grumnudlem  44254  uzmptshftfval  44315  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  rabexgf  44924  uzct  44965  disjf1o  45098  dmmptssf  45139  mptssid  45149  uzfissfz  45241  ssuzfz  45264  uzssre2  45322  uzublem  45345  uzssz2  45371  uzsscn2  45393  sumnnodd  45551  climconstmpt  45579  fnlimfvre  45595  fnlimabslt  45600  limsupvaluz  45629  limsupubuzlem  45633  limsupubuz  45634  limsupequzmpt2  45639  limsupmnfuzlem  45647  limsupre3uzlem  45656  liminfequzmpt2  45712  ibliooicc  45892  stoweidlem44  45965  stoweidlem50  45971  stoweidlem51  45972  stoweidlem52  45973  stoweidlem57  45978  stoweidlem59  45980  fourierdlem16  46044  fourierdlem19  46047  fourierdlem21  46049  fourierdlem22  46050  fourierdlem42  46070  fourierdlem83  46110  fouriersw  46152  salexct  46255  salexct3  46263  salgencntex  46264  salgensscntex  46265  sge0less  46313  sge0fodjrnlem  46337  sge0isum  46348  ovnlerp  46483  ovn0lem  46486  hoidmv1lelem1  46512  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  ovnhoilem1  46522  ovnhoilem2  46523  opnvonmbllem2  46554  ovolval4lem1  46570  ovolval5lem3  46575  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  incsmflem  46662  decsmflem  46687  smflimlem2  46693  smflimlem3  46694  smflim  46698  smfrec  46710  smfmullem4  46715  smfdiv  46718  smfsuplem1  46732  smfsuplem3  46734  smfsupxr  46737  smfliminflem  46751  cfsetssfset  46971  fcoreslem2  46979  fcores  46982  gricrel  47772  clnbgrisubgrgrim  47784  grlimgrtrilem2  47819  grlicrel  47823  oddibas  47896  2zlidl  47963  2zrngbas  47965  2zrng0  47967  fldcALTV  48055  fldhmsubcALTV  48056  ipolub0  48664