Theorem eqsstri 3635

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)

Hypotheses

Ref	Expression
eqsstr.1	|- A = B
eqsstr.2	|- B C_ C

Assertion

Ref	Expression
eqsstri	|- A C_ C

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 |- B C_ C
2		eqsstr.1	. . 3 |- A = B
3	2	sseq1i 3629	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	mpbir 221	1 |- A C_ C

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqsstr3i  3636  ssrab2  3687  ssrab3  3688  rabssab  3690  opabss  4714  brab2a  5194  relopabiALT  5246  dmopabss  5336  resss  5422  relres  5426  rnin  5542  rnxpss  5566  cnvcnvss  5589  dmmptss  5631  predss  5687  fnres  6007  f0  6086  nfvres  6224  fvopab4ndm  6307  ffvresb  6394  mptexgf  6485  funiunfv  6506  isoini2  6589  ovssunirn  6681  dmoprabss  6742  mpt2ndm0  6875  elmpt2cl  6876  omsson  7069  exse2  7105  fabexg  7122  frxp  7287  tposssxp  7356  dftpos4  7371  wfrdmss  7421  smores  7449  smores2  7451  iordsmo  7454  oawordeulem  7634  swoer  7772  swoord1  7773  swoord2  7774  ecss  7788  ecopovsym  7849  ecopovtrn  7850  ecopover  7851  ecopoverOLD  7852  sbthlem7  8076  nnfi  8153  imafi  8259  elfiun  8336  marypha1lem  8339  marypha2lem1  8341  ordtypelem2  8424  hartogslem1  8447  wemapso2lem  8457  wdomima2g  8491  inf3lem1  8525  wemapwe  8594  tc2  8618  tz9.12lem1  8650  rankuni  8726  rankuniss  8729  rankmapu  8741  cplem1  8752  hta  8760  r0weon  8835  infxpenlem  8836  ackbij1lem9  9050  ackbij1lem10  9051  ackbij1b  9061  cofsmo  9091  sdom2en01  9124  fin23lem26  9147  fin23lem28  9162  fin23lem30  9164  isf32lem5  9179  isf32lem6  9180  isf32lem7  9181  isf32lem8  9182  fin56  9215  fin1a2lem9  9230  hsmexlem4  9251  hsmexlem5  9252  hsmexlem6  9253  axdc3lem  9272  axdc3lem2  9273  axcclem  9279  zorn2lem1  9318  zorn2lem3  9320  zorn2lem4  9321  zorn2lem5  9322  imadomg  9356  iundom2g  9362  smobeth  9408  canth4  9469  gruina  9640  grur1a  9641  pinn  9700  niex  9703  ltsopi  9710  ltrelpi  9711  dmaddpi  9712  dmmulpi  9713  enqex  9744  0nnq  9746  elpqn  9747  ltrelnq  9748  nqerf  9752  nqerrel  9754  dmrecnq  9790  lterpq  9792  ltrelpr  9820  enrex  9888  ltrelsr  9889  dmaddsr  9906  dmmulsr  9907  ltrelre  9955  axaddf  9966  axmulf  9967  ltrelxr  10099  lerelxr  10101  nn0ssre  11296  nn0ssz  11398  uzsupss  11780  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  rpre  11839  uzsup  12662  fzfi  12771  swrd00  13418  sqrlem3  13985  sqrlem5  13987  cau3  14095  caubnd  14098  limsupgre  14212  rlimpm  14231  rlimclim  14277  isercolllem1  14395  isercolllem2  14396  isercoll  14398  caurcvg  14407  caucvg  14409  iseraltlem2  14413  iseraltlem3  14414  zsum  14449  fsumcvg3  14460  climfsum  14552  ackbijnn  14560  divcnvshft  14587  infcvgaux1i  14589  clim2prod  14620  ntrivcvg  14629  ntrivcvgfvn0  14631  ntrivcvgtail  14632  ntrivcvgmullem  14633  ntrivcvgmul  14634  zprod  14667  dvdszrcl  14988  dvdsflip  15039  divalglem2  15118  divalglem5  15120  divalglem8  15123  gcdcllem3  15223  bezoutlem2  15257  bezoutlem3  15258  maxprmfct  15421  phimullem  15484  eulerthlem2  15487  prmdiveq  15491  prmdivdiv  15492  pclem  15543  infpn2  15617  prmreclem2  15621  prmreclem3  15622  prmreclem5  15624  4sqlem1  15652  4sqlem13  15661  4sqlem14  15662  4sqlem17  15665  4sqlem18  15666  4sqlem19  15667  vdwnnlem3  15701  ramcl2lem  15713  ramtcl  15714  ramtcl2  15715  ramtub  15716  ramub1lem2  15731  structcnvcnv  15871  fvsetsid  15890  strlemor0OLD  15968  strlemor1OLD  15969  strleun  15972  imasdsval2  16176  gsumval1  17277  nmzsubg  17635  nmznsg  17638  conjnmz  17694  conjnmzb  17695  gicer  17718  gicerOLD  17719  gastacl  17742  symgbasfi  17806  mvdco  17865  symgsssg  17887  sylow1lem2  18014  sylow1lem3  18015  sylow1lem4  18016  sylow1lem5  18017  sylow2a  18034  sylow3lem2  18043  efglem  18129  efgtf  18135  efgtlen  18139  efginvrel2  18140  efginvrel1  18141  efgsfo  18152  efgredlemg  18155  efgredleme  18156  efgredlemd  18157  efgredlemc  18158  efgredlem  18160  efgred  18161  efgrelexlemb  18163  efgcpbllemb  18168  frgpinv  18177  frgpuplem  18185  frgpupf  18186  frgpup1  18188  frgpnabllem2  18277  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  ablfacrplem  18464  ablfacrp2  18466  ablfac1eu  18472  pgpfaclem1  18480  ablfaclem2  18485  ablfaclem3  18486  lspsolvlem  19142  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  rrgeq0  19290  rrgss  19292  psrbagconf1o  19374  psrass1lem  19377  mplbasss  19432  ply1bascl  19573  coe1mul2lem2  19638  znf1o  19900  zntoslem  19905  cygznlem2a  19916  psgnghm  19926  pjpm  20052  dsmmbase  20079  frlmsslsp  20135  dmtopon  20727  mretopd  20896  ordtbas  20996  leordtval2  21016  lecldbas  21023  lmfval  21036  lmbrf  21064  cnconst2  21087  hauscmplem  21209  conncompcld  21237  hauspwdom  21304  txuni2  21368  xkouni  21402  xkoccn  21422  txkgen  21455  qtoptop2  21502  kqdisj  21535  hmphtop  21581  hmpher  21587  uzrest  21701  uzfbas  21702  lmflf  21809  ptcmplem1  21856  ptcmplem3  21858  tgpconncompeqg  21915  tgpconncomp  21916  ustn0  22024  imasdsf1olem  22178  xmeter  22238  blcld  22310  isngp2  22401  xrtgioo  22609  iccntr  22624  icccmplem1  22625  icccmplem2  22626  icccmplem3  22627  xmetdcn  22641  metdcn  22643  metdscn2  22660  icchmeo  22740  cnheiborlem  22753  lmmbrf  23060  iscau4  23077  iscauf  23078  caucfil  23081  lmclimf  23102  rrxf  23184  ivthlem1  23220  ivthlem2  23221  ivthlem3  23222  ovolsslem  23252  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicc2  23290  volf  23297  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  dyadmbllem  23367  dyadmbl  23368  volcn  23374  mbfimaopnlem  23422  mbflimsup  23433  i1f1  23457  itg2lcl  23494  iblmbf  23534  itgioo  23582  itgsplitioo  23604  limcflflem  23644  limcflf  23645  limcresi  23649  lhop  23779  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlimge0  23793  dvfsumrlim  23794  dvfsumrlim2  23795  dvfsum2  23797  vieta1lem1  24065  vieta1lem2  24066  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  pserdv2  24184  abelthlem4  24188  abelthlem6  24190  abelthlem9  24194  abelth  24195  logcnlem5  24392  dvlog  24397  dvlog2lem  24398  dvlog2  24399  dvcncxp1  24484  dvcnsqrt  24485  cxpcn3lem  24488  cxpcn3  24489  sqrtcn  24491  1cubr  24569  atansssdm  24660  atancn  24663  jensen  24715  lgamucov  24764  lgamucov2  24765  wilthlem1  24794  ftalem3  24801  musum  24917  dvdsmulf1o  24920  fsumdvdsmul  24921  ppiub  24929  lgsfcl2  25028  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  2sqlem7  25149  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  pntlem3  25298  axtgcgrrflx  25361  axtgcgrid  25362  axtgsegcon  25363  axtg5seg  25364  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  tglng  25441  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  axcontlem10  25853  upgrreslem  26196  umgrreslem  26197  vtxdginducedm1lem2  26436  finsumvtxdg2ssteplem1  26441  disjxwwlkn  26808  clwwlknclwwlkdifnum  26874  clwwlkssswrd  26911  frgrwopreg2  27183  phnv  27669  htthlem  27774  hlimadd  28050  hlimcaui  28093  hhsscms  28136  occllem  28162  shjshsi  28351  3oalem4  28524  pjfi  28563  dmadjss  28746  nlelshi  28919  nlelchi  28920  hmopidmchi  29010  atssch  29202  shatomistici  29220  fcoinver  29418  mptctf  29495  fcobijfs  29501  psgnfzto1stlem  29850  cnre2csqima  29957  raddcn  29975  rrhre  30065  esumsnf  30126  sxbrsiga  30352  omssubadd  30362  carsggect  30380  sitmcl  30413  oddpwdc  30416  eulerpartlem1  30429  eulerpartlemt  30433  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpartlemgh  30440  sseqf  30454  ballotlemfmpn  30556  ballotth  30599  signswch  30638  ftc2re  30676  fdvposlt  30677  fdvposle  30679  bnj1146  30862  bnj1292  30886  bnj1293  30887  bnj1145  31061  bnj1177  31074  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem2  31174  kur14lem3  31190  kur14lem6  31193  kur14lem7  31194  kur14lem9  31196  cvmlift2lem12  31296  mpstssv  31436  mstapst  31444  mppspstlem  31468  mppspst  31471  mthmsta  31475  mthmpps  31479  mclsppslem  31480  dfpo2  31645  wlimss  31778  frrlem7  31790  nosupbnd1lem1  31854  nosupbnd2  31862  scutf  31919  txpss3v  31985  pprodss4v  31991  relsset  31995  fixssdm  32013  fixssrn  32014  limitssson  32018  funpartss  32051  colinearex  32167  fneer  32348  neibastop1  32354  neibastop2lem  32355  filnetlem2  32374  filnetlem3  32375  knoppcnlem10  32492  bj-tagss  32968  bj-cmnssmnd  33136  bj-ablssgrp  33138  bj-ablsscmn  33140  bj-vecssmod  33143  bj-rrvecssvec  33150  icoreresf  33200  icoreunrn  33207  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimir  33442  broucube  33443  dvasin  33496  dvacos  33497  areacirc  33505  caures  33556  bnd2lem  33590  ismtyres  33607  flddivrng  33798  xrnss3v  34135  toycom  34260  dihglblem2N  36583  lcdvbase  36882  mapdunirnN  36939  eldiophb  37320  monotuz  37506  fglmod  37643  pwssplit4  37659  pwfi2f1o  37666  arearect  37801  fvnonrel  37903  rclexi  37922  rtrclex  37924  trclexi  37927  rtrclexi  37928  clcnvlem  37930  cnvrcl0  37932  cnvtrcl0  37933  dfrtrcl5  37936  dfrcl2  37966  comptiunov2i  37998  corclrcl  37999  trclrelexplem  38003  relexpaddss  38010  cotrcltrcl  38017  corcltrcl  38031  cotrclrcl  38034  frege131d  38056  rp-imass  38065  0he  38076  uzmptshftfval  38545  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  rabexgf  39183  uzct  39232  disjf1o  39378  dmresss  39436  dmmptssf  39438  mptssid  39450  fz1ssfz0  39524  uzfissfz  39542  ssuzfz  39565  uzssre2  39633  uzublem  39657  uzssz2  39685  uzsscn2  39708  limcperiod  39860  sumnnodd  39862  climconstmpt  39890  fnlimfvre  39906  fnlimabslt  39911  limsupvaluz  39940  limsupubuzlem  39944  limsupubuz  39945  limsupequzmpt2  39950  limsupmnfuzlem  39958  limsupre3uzlem  39967  liminfequzmpt2  40023  cncfshift  40087  cncfperiod  40092  ibliooicc  40187  stoweidlem26  40243  stoweidlem44  40261  stoweidlem50  40267  stoweidlem51  40268  stoweidlem52  40269  stoweidlem57  40274  stoweidlem59  40276  fourierdlem16  40340  fourierdlem19  40343  fourierdlem21  40345  fourierdlem22  40346  fourierdlem42  40366  fourierdlem83  40406  fouriersw  40448  salexct  40552  salexct3  40560  salgencntex  40561  salgensscntex  40562  sge0less  40609  sge0fodjrnlem  40633  sge0isum  40644  ovnsslelem  40774  ovnlerp  40776  ovn0lem  40779  hoidmv1lelem1  40805  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  ovnhoilem1  40815  ovnhoilem2  40816  opnvonmbllem2  40847  ovolval4lem1  40863  ovolval5lem3  40868  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  incsmflem  40950  decsmflem  40974  smflimlem2  40980  smflimlem3  40981  smflim  40985  smfrec  40996  smfmullem4  41001  smfdiv  41004  smfsuplem1  41017  smfsuplem3  41019  smfsupxr  41022  smfliminflem  41036  oddibas  41813  2zlidl  41934  2zrngbas  41936  2zrng0  41938  fldc  42083  fldhmsubc  42084  fldcALTV  42101  fldhmsubcALTV  42102  setrec2lem1  42440