Theorem eqsstri 3951

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

Syntax hints:   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqsstrri  3952  ssrab2OLD  4010  ssrab3  4011  rabssab  4014  ifssun  4473  opabss  5134  brab2a  5670  relopabiALT  5722  dmopabss  5816  resss  5905  relres  5909  rnin  6039  rnxpss  6064  cnvcnvss  6086  resdmss  6127  resssxp  6162  dfpo2  6188  predss  6199  fnres  6543  f0  6639  nfvres  6792  fvopab4ndm  6886  ffvresb  6980  mptexgf  7080  funiunfv  7103  isoini2  7190  ovssunirn  7291  dmoprabss  7355  mpondm0  7488  elmpocl  7489  exse2  7738  fabexg  7755  frxp  7938  tposssxp  8017  dftpos4  8032  wfrdmssOLD  8117  smores  8154  smores2  8156  iordsmo  8159  swoer  8486  swoord1  8487  swoord2  8488  ecss  8502  ecopovsym  8566  ecopovtrn  8567  ecopover  8568  f1setex  8603  sbthlem7  8829  nnfiOLD  8946  imafiALT  9042  elfiun  9119  marypha1lem  9122  marypha2lem1  9124  hartogslem1  9231  wdomima2g  9275  inf3lem1  9316  tc2  9431  tz9.12lem1  9476  rankuni  9552  rankuniss  9555  rankmapu  9567  hta  9586  r0weon  9699  infxpenlem  9700  ackbij1lem9  9915  ackbij1lem10  9916  ackbij1b  9926  sdom2en01  9989  fin23lem26  10012  fin56  10080  fin1a2lem9  10095  axdc3lem  10137  axdc3lem2  10138  axcclem  10144  imadomg  10221  iundom2g  10227  smobeth  10273  canth4  10334  gruina  10505  grur1a  10506  pinn  10565  niex  10568  ltsopi  10575  ltrelpi  10576  dmaddpi  10577  dmmulpi  10578  enqex  10609  ltrelnq  10613  nqerf  10617  nqerrel  10619  dmrecnq  10655  lterpq  10657  ltrelpr  10685  enrex  10754  ltrelsr  10755  dmaddsr  10772  dmmulsr  10773  ltrelre  10821  axaddf  10832  axmulf  10833  ltrelxr  10967  lerelxr  10969  nn0ssre  12167  nn0sscn  12168  nn0ssz  12271  uzsupss  12609  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  fz1ssfz0  13281  uzsup  13511  fzfi  13620  swrd00  14285  sqrlem3  14884  cau3  14995  caubnd  14998  limsupgre  15118  rlimpm  15137  rlimclim  15183  isercolllem1  15304  isercolllem2  15305  isercoll  15307  caurcvg  15316  caucvg  15318  iseraltlem2  15322  iseraltlem3  15323  zsum  15358  fsumcvg3  15369  climfsum  15460  ackbijnn  15468  divcnvshft  15495  infcvgaux1i  15497  clim2prod  15528  ntrivcvg  15537  ntrivcvgfvn0  15539  ntrivcvgtail  15540  ntrivcvgmullem  15541  ntrivcvgmul  15542  zprod  15575  dvdszrcl  15896  4sqlem1  16577  4sqlem19  16592  ramub1lem2  16656  structcnvcnv  16782  strleun  16786  fvsetsid  16797  smndex1sgrp  18462  gicer  18807  symgbasfi  18901  mvdco  18968  symgsssg  18990  efglem  19237  efgtf  19243  efgtlen  19247  efginvrel2  19248  efginvrel1  19249  efgsfo  19260  efgredlemg  19263  efgredleme  19264  efgredlemd  19265  efgredlemc  19266  efgredlem  19268  efgred  19269  efgrelexlemb  19271  efgcpbllemb  19276  frgpinv  19285  frgpuplem  19293  frgpupf  19294  frgpup1  19296  frgpnabllem2  19390  gsumval3lem1  19421  gsumval3lem2  19422  gsumval3  19423  lbsextlem3  20337  znf1o  20671  zntoslem  20676  pjpm  20825  mhp0cl  21246  ply1bascl  21284  dmtopon  21980  ordtbas  22251  leordtval2  22271  lecldbas  22278  lmfval  22291  lmbrf  22319  cnconst2  22342  conncompcld  22493  hauspwdom  22560  txuni2  22624  xkouni  22658  xkoccn  22678  txkgen  22711  qtoptop2  22758  kqdisj  22791  hmphtop  22837  hmpher  22843  uzrest  22956  uzfbas  22957  lmflf  23064  tgpconncompeqg  23171  tgpconncomp  23172  ustn0  23280  xmeter  23494  isngp2  23659  xrtgioo  23875  iccntr  23890  xmetdcn  23907  metdcn  23909  metdscn2  23926  icchmeo  24010  cnheiborlem  24023  lmmbrf  24331  iscau4  24348  iscauf  24349  caucfil  24352  lmclimf  24373  volf  24598  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  volcn  24675  mbfimaopnlem  24724  mbflimsup  24735  i1f1  24759  itg2lcl  24797  itgioo  24885  itgsplitioo  24907  limcflflem  24949  limcflf  24950  limcresi  24954  lhop  25085  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsumrlimge0  25099  dvfsumrlim  25100  dvfsumrlim2  25101  dvfsum2  25103  vieta1lem1  25375  vieta1lem2  25376  psercnlem2  25488  psercnlem1  25489  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  pserdv  25493  pserdv2  25494  logcnlem5  25706  dvlog  25711  dvlog2lem  25712  dvlog2  25713  dvcncxp1  25801  dvcnsqrt  25802  cxpcn3lem  25805  cxpcn3  25806  sqrtcn  25808  1cubr  25897  atansssdm  25988  jensen  26043  musum  26245  ppiub  26257  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  2sqlem7  26477  axtgcgrrflx  26727  axtgcgrid  26728  axtgsegcon  26729  axtg5seg  26730  axtgbtwnid  26731  axtgpasch  26732  axtgcont1  26733  tglng  26811  disjxwwlkn  28179  frgrwopreg2  28584  phnv  29077  htthlem  29180  hlimadd  29456  hlimcaui  29499  hhsscms  29541  occllem  29566  shjshsi  29755  3oalem4  29928  pjfi  29967  dmadjss  30150  nlelshi  30323  nlelchi  30324  hmopidmchi  30414  shatomistici  30624  difxp1ss  30771  difxp2ss  30772  fcoinver  30847  opabssi  30854  mptctf  30954  gsumpart  31217  pmtrcnel2  31261  psgnfzto1stlem  31269  cycpmrn  31312  cyc3genpm  31321  lsmsnorb  31481  cnre2csqima  31763  raddcn  31781  rrhre  31871  esumsnf  31932  sxbrsiga  32157  omssubadd  32167  carsggect  32185  sitmcl  32218  oddpwdc  32221  eulerpartlem1  32234  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemmf  32242  eulerpartlemgh  32245  sseqf  32259  ballotlemfmpn  32361  ballotth  32404  signswch  32440  ftc2re  32478  fdvposlt  32479  fdvposle  32481  bnj1146  32671  bnj1292  32695  bnj1293  32696  bnj1145  32873  bnj1177  32886  erdszelem2  33054  kur14lem3  33070  kur14lem6  33073  kur14lem7  33074  kur14lem9  33076  cvmlift2lem12  33176  mpstssv  33401  mstapst  33409  mppspstlem  33433  mppspst  33436  mthmsta  33440  mthmpps  33444  mclsppslem  33445  dmttrcl  33707  rnttrcl  33708  nosupbnd1lem1  33838  nosupbnd2  33846  noinfbnd1lem1  33853  scutf  33933  leftssold  33988  rightssold  33989  txpss3v  34107  pprodss4v  34113  relsset  34117  fixssdm  34135  fixssrn  34136  limitssson  34140  funpartss  34173  colinearex  34289  fneer  34469  neibastop1  34475  neibastop2lem  34476  filnetlem2  34495  filnetlem3  34496  knoppcnlem10  34609  bj-tagss  35097  bj-imdirco  35288  bj-fvsnun2  35354  bj-ablssgrp  35374  bj-ablsscmn  35376  bj-vecssmod  35379  bj-fldssdrng  35386  icoreresf  35450  icoreunrn  35457  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimir  35737  broucube  35738  dvasin  35788  dvacos  35789  areacirc  35797  caures  35845  bnd2lem  35876  ismtyres  35893  flddivrng  36084  xrnss3v  36429  refrelsredund2  36673  toycom  36914  dihglblem2N  39235  lcdvbase  39534  mapdunirnN  39591  prjspreln0  40369  prjspvs  40370  prjspeclsp  40372  0prjspnrel  40385  dffltz  40387  eldiophb  40495  monotuz  40679  pwssplit4  40830  pwfi2f1o  40837  arearect  40962  fvnonrel  41094  rclexi  41112  rtrclex  41114  trclexi  41117  rtrclexi  41118  clcnvlem  41120  cnvrcl0  41122  cnvtrcl0  41123  dfrtrcl5  41126  dfrcl2  41171  comptiunov2i  41203  corclrcl  41204  trclrelexplem  41208  relexpaddss  41215  cotrcltrcl  41222  corcltrcl  41236  cotrclrcl  41239  frege131d  41261  0he  41279  grumnudlem  41792  uzmptshftfval  41853  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  rabexgf  42456  uzct  42500  disjf1o  42618  dmresss  42663  dmmptssf  42664  mptssid  42674  uzfissfz  42755  ssuzfz  42778  uzssre2  42837  uzublem  42860  uzssz2  42886  uzsscn2  42908  sumnnodd  43061  climconstmpt  43089  fnlimfvre  43105  fnlimabslt  43110  limsupvaluz  43139  limsupubuzlem  43143  limsupubuz  43144  limsupequzmpt2  43149  limsupmnfuzlem  43157  limsupre3uzlem  43166  liminfequzmpt2  43222  ibliooicc  43402  stoweidlem44  43475  stoweidlem50  43481  stoweidlem51  43482  stoweidlem52  43483  stoweidlem57  43488  stoweidlem59  43490  fourierdlem16  43554  fourierdlem19  43557  fourierdlem21  43559  fourierdlem22  43560  fourierdlem42  43580  fourierdlem83  43620  fouriersw  43662  salexct  43763  salexct3  43771  salgencntex  43772  salgensscntex  43773  sge0less  43820  sge0fodjrnlem  43844  sge0isum  43855  ovnsslelem  43988  ovnlerp  43990  ovn0lem  43993  hoidmv1lelem1  44019  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  ovnhoilem1  44029  ovnhoilem2  44030  opnvonmbllem2  44061  ovolval4lem1  44077  ovolval5lem3  44082  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  incsmflem  44164  decsmflem  44188  smflimlem2  44194  smflimlem3  44195  smflim  44199  smfrec  44210  smfmullem4  44215  smfdiv  44218  smfsuplem1  44231  smfsuplem3  44233  smfsupxr  44236  smfliminflem  44250  cfsetssfset  44437  fcoreslem2  44445  fcores  44448  oddibas  45255  2zlidl  45380  2zrngbas  45382  2zrng0  45384  fldc  45529  fldhmsubc  45530  fldcALTV  45547  fldhmsubcALTV  45548  ipolub0  46166