MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstri Structured version   Visualization version   GIF version

Theorem eqsstri 3633
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
StepHypRef Expression
1 eqsstr.2 . 2 𝐵𝐶
2 eqsstr.1 . . 3 𝐴 = 𝐵
32sseq1i 3627 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 221 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1482  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3579  df-ss 3586
This theorem is referenced by:  eqsstr3i  3634  ssrab2  3685  ssrab3  3686  rabssab  3688  opabss  4712  brab2a  5192  relopabiALT  5244  dmopabss  5334  resss  5420  relres  5424  rnin  5540  rnxpss  5564  cnvcnvss  5587  dmmptss  5629  predss  5685  fnres  6005  f0  6084  nfvres  6222  fvopab4ndm  6305  ffvresb  6392  mptexgf  6482  funiunfv  6503  isoini2  6586  ovssunirn  6678  dmoprabss  6739  mpt2ndm0  6872  elmpt2cl  6873  omsson  7066  exse2  7102  fabexg  7119  frxp  7284  tposssxp  7353  dftpos4  7368  wfrdmss  7418  smores  7446  smores2  7448  iordsmo  7451  oawordeulem  7631  swoer  7769  swoord1  7770  swoord2  7771  ecss  7785  ecopovsym  7846  ecopovtrn  7847  ecopover  7848  ecopoverOLD  7849  sbthlem7  8073  nnfi  8150  imafi  8256  elfiun  8333  marypha1lem  8336  marypha2lem1  8338  ordtypelem2  8421  hartogslem1  8444  wemapso2lem  8454  wdomima2g  8488  inf3lem1  8522  wemapwe  8591  tc2  8615  tz9.12lem1  8647  rankuni  8723  rankuniss  8726  rankmapu  8738  cplem1  8749  hta  8757  r0weon  8832  infxpenlem  8833  ackbij1lem9  9047  ackbij1lem10  9048  ackbij1b  9058  cofsmo  9088  sdom2en01  9121  fin23lem26  9144  fin23lem28  9159  fin23lem30  9161  isf32lem5  9176  isf32lem6  9177  isf32lem7  9178  isf32lem8  9179  fin56  9212  fin1a2lem9  9227  hsmexlem4  9248  hsmexlem5  9249  hsmexlem6  9250  axdc3lem  9269  axdc3lem2  9270  axcclem  9276  zorn2lem1  9315  zorn2lem3  9317  zorn2lem4  9318  zorn2lem5  9319  imadomg  9353  iundom2g  9359  smobeth  9405  canth4  9466  gruina  9637  grur1a  9638  pinn  9697  niex  9700  ltsopi  9707  ltrelpi  9708  dmaddpi  9709  dmmulpi  9710  enqex  9741  0nnq  9743  elpqn  9744  ltrelnq  9745  nqerf  9749  nqerrel  9751  dmrecnq  9787  lterpq  9789  ltrelpr  9817  enrex  9885  ltrelsr  9886  dmaddsr  9903  dmmulsr  9904  ltrelre  9952  axaddf  9963  axmulf  9964  ltrelxr  10096  lerelxr  10098  nn0ssre  11293  nn0ssz  11395  uzsupss  11777  rpnnen1lem2  11811  rpnnen1lem1  11812  rpnnen1lem3  11813  rpnnen1lem5  11815  rpnnen1lem1OLD  11818  rpnnen1lem3OLD  11819  rpnnen1lem5OLD  11821  rpre  11836  uzsup  12657  fzfi  12766  swrd00  13412  sqrlem3  13979  sqrlem5  13981  cau3  14089  caubnd  14092  limsupgre  14206  rlimpm  14225  rlimclim  14271  isercolllem1  14389  isercolllem2  14390  isercoll  14392  caurcvg  14401  caucvg  14403  iseraltlem2  14407  iseraltlem3  14408  zsum  14443  fsumcvg3  14454  climfsum  14546  ackbijnn  14554  divcnvshft  14581  infcvgaux1i  14583  clim2prod  14614  ntrivcvg  14623  ntrivcvgfvn0  14625  ntrivcvgtail  14626  ntrivcvgmullem  14627  ntrivcvgmul  14628  zprod  14661  dvdszrcl  14982  dvdsflip  15033  divalglem2  15112  divalglem5  15114  divalglem8  15117  gcdcllem3  15217  bezoutlem2  15251  bezoutlem3  15252  maxprmfct  15415  phimullem  15478  eulerthlem2  15481  prmdiveq  15485  prmdivdiv  15486  pclem  15537  infpn2  15611  prmreclem2  15615  prmreclem3  15616  prmreclem5  15618  4sqlem1  15646  4sqlem13  15655  4sqlem14  15656  4sqlem17  15659  4sqlem18  15660  4sqlem19  15661  vdwnnlem3  15695  ramcl2lem  15707  ramtcl  15708  ramtcl2  15709  ramtub  15710  ramub1lem2  15725  structcnvcnv  15865  fvsetsid  15884  strlemor0OLD  15962  strlemor1OLD  15963  strleun  15966  imasdsval2  16170  gsumval1  17271  nmzsubg  17629  nmznsg  17632  conjnmz  17688  conjnmzb  17689  gicer  17712  gicerOLD  17713  gastacl  17736  symgbasfi  17800  mvdco  17859  symgsssg  17881  sylow1lem2  18008  sylow1lem3  18009  sylow1lem4  18010  sylow1lem5  18011  sylow2a  18028  sylow3lem2  18037  efglem  18123  efgtf  18129  efgtlen  18133  efginvrel2  18134  efginvrel1  18135  efgsfo  18146  efgredlemg  18149  efgredleme  18150  efgredlemd  18151  efgredlemc  18152  efgredlem  18154  efgred  18155  efgrelexlemb  18157  efgcpbllemb  18162  frgpinv  18171  frgpuplem  18179  frgpupf  18180  frgpup1  18182  frgpnabllem2  18271  gsumval3lem1  18300  gsumval3lem2  18301  gsumval3  18302  ablfacrplem  18458  ablfacrp2  18460  ablfac1eu  18466  pgpfaclem1  18474  ablfaclem2  18479  ablfaclem3  18480  lspsolvlem  19136  lbsextlem2  19153  lbsextlem3  19154  lbsextlem4  19155  rrgeq0  19284  rrgss  19286  psrbagconf1o  19368  psrass1lem  19371  mplbasss  19426  ply1bascl  19567  coe1mul2lem2  19632  znf1o  19894  zntoslem  19899  cygznlem2a  19910  psgnghm  19920  pjpm  20046  dsmmbase  20073  frlmsslsp  20129  dmtopon  20721  mretopd  20890  ordtbas  20990  leordtval2  21010  lecldbas  21017  lmfval  21030  lmbrf  21058  cnconst2  21081  hauscmplem  21203  conncompcld  21231  hauspwdom  21298  txuni2  21362  xkouni  21396  xkoccn  21416  txkgen  21449  qtoptop2  21496  kqdisj  21529  hmphtop  21575  hmpher  21581  uzrest  21695  uzfbas  21696  lmflf  21803  ptcmplem1  21850  ptcmplem3  21852  tgpconncompeqg  21909  tgpconncomp  21910  ustn0  22018  imasdsf1olem  22172  xmeter  22232  blcld  22304  isngp2  22395  xrtgioo  22603  iccntr  22618  icccmplem1  22619  icccmplem2  22620  icccmplem3  22621  xmetdcn  22635  metdcn  22637  metdscn2  22654  icchmeo  22734  cnheiborlem  22747  lmmbrf  23054  iscau4  23071  iscauf  23072  caucfil  23075  lmclimf  23096  rrxf  23178  ivthlem1  23214  ivthlem2  23215  ivthlem3  23216  ovolsslem  23246  ovolicc2lem3  23281  ovolicc2lem4  23282  ovolicc2lem5  23283  ovolicc2  23284  volf  23291  uniioombllem3  23347  uniioombllem4  23348  uniioombllem5  23349  dyadmbllem  23361  dyadmbl  23362  volcn  23368  mbfimaopnlem  23416  mbflimsup  23427  i1f1  23451  itg2lcl  23488  iblmbf  23528  itgioo  23576  itgsplitioo  23598  limcflflem  23638  limcflf  23639  limcresi  23643  lhop  23773  dvfsumlem1  23783  dvfsumlem2  23784  dvfsumlem3  23785  dvfsumlem4  23786  dvfsumrlimge0  23787  dvfsumrlim  23788  dvfsumrlim2  23789  dvfsum2  23791  vieta1lem1  24059  vieta1lem2  24060  psercnlem2  24172  psercnlem1  24173  psercn  24174  pserdvlem1  24175  pserdvlem2  24176  pserdv  24177  pserdv2  24178  abelthlem4  24182  abelthlem6  24184  abelthlem9  24188  abelth  24189  logcnlem5  24386  dvlog  24391  dvlog2lem  24392  dvlog2  24393  dvcncxp1  24478  dvcnsqrt  24479  cxpcn3lem  24482  cxpcn3  24483  sqrtcn  24485  1cubr  24563  atansssdm  24654  atancn  24657  jensen  24709  lgamucov  24758  lgamucov2  24759  wilthlem1  24788  ftalem3  24795  musum  24911  dvdsmulf1o  24914  fsumdvdsmul  24915  ppiub  24923  lgsfcl2  25022  lgsquadlem1  25099  lgsquadlem2  25100  lgsquadlem3  25101  2sqlem7  25143  rpvmasum2  25195  dchrisum0re  25196  dchrisum0lema  25197  dchrisum0lem1b  25198  dchrisum0lem1  25199  dchrisum0lem2a  25200  dchrisum0lem2  25201  dchrisum0lem3  25202  dchrisum0  25203  pntlem3  25292  axtgcgrrflx  25355  axtgcgrid  25356  axtgsegcon  25357  axtg5seg  25358  axtgbtwnid  25359  axtgpasch  25360  axtgcont1  25361  tglng  25435  axcontlem2  25839  axcontlem7  25844  axcontlem8  25845  axcontlem10  25847  upgrreslem  26190  umgrreslem  26191  vtxdginducedm1lem2  26430  finsumvtxdg2ssteplem1  26435  disjxwwlkn  26802  clwwlknclwwlkdifnum  26868  clwwlkssswrd  26904  frgrwopreg1  27173  frgrwopreg2  27174  phnv  27653  htthlem  27758  hlimadd  28034  hlimcaui  28077  hhsscms  28120  occllem  28146  shjshsi  28335  3oalem4  28508  pjfi  28547  dmadjss  28730  nlelshi  28903  nlelchi  28904  hmopidmchi  28994  atssch  29186  shatomistici  29204  fcoinver  29402  mptctf  29480  fcobijfs  29486  psgnfzto1stlem  29835  cnre2csqima  29942  raddcn  29960  rrhre  30050  esumsnf  30111  sxbrsiga  30337  omssubadd  30347  carsggect  30365  sitmcl  30398  oddpwdc  30401  eulerpartlem1  30414  eulerpartlemt  30418  eulerpartgbij  30419  eulerpartlemmf  30422  eulerpartlemgvv  30423  eulerpartlemgh  30425  sseqf  30439  ballotlemfmpn  30541  ballotth  30584  signswch  30623  ftc2re  30661  fdvposlt  30662  fdvposle  30664  bnj1146  30847  bnj1292  30871  bnj1293  30872  bnj1145  31046  bnj1177  31059  subfacp1lem3  31149  subfacp1lem5  31151  erdszelem2  31159  kur14lem3  31175  kur14lem6  31178  kur14lem7  31179  kur14lem9  31181  cvmlift2lem12  31281  mpstssv  31421  mstapst  31429  mppspstlem  31453  mppspst  31456  mthmsta  31460  mthmpps  31464  mclsppslem  31465  dfpo2  31631  wlimss  31762  frrlem7  31774  nosupbnd1lem1  31838  nosupbnd2  31846  scutf  31903  txpss3v  31969  pprodss4v  31975  relsset  31979  fixssdm  31997  fixssrn  31998  limitssson  32002  funpartss  32035  colinearex  32151  fneer  32332  neibastop1  32338  neibastop2lem  32339  filnetlem2  32358  filnetlem3  32359  knoppcnlem10  32476  bj-tagss  32952  bj-cmnssmnd  33116  bj-ablssgrp  33118  bj-ablsscmn  33120  bj-vecssmod  33123  bj-rrvecssvec  33130  icoreresf  33180  icoreunrn  33187  poimirlem29  33418  poimirlem30  33419  poimirlem31  33420  poimir  33422  broucube  33423  dvasin  33476  dvacos  33477  areacirc  33485  caures  33536  bnd2lem  33570  ismtyres  33587  flddivrng  33778  toycom  34086  dihglblem2N  36409  lcdvbase  36708  mapdunirnN  36765  eldiophb  37146  monotuz  37332  fglmod  37469  pwssplit4  37485  pwfi2f1o  37492  arearect  37627  fvnonrel  37729  rclexi  37748  rtrclex  37750  trclexi  37753  rtrclexi  37754  clcnvlem  37756  cnvrcl0  37758  cnvtrcl0  37759  dfrtrcl5  37762  dfrcl2  37792  comptiunov2i  37824  corclrcl  37825  trclrelexplem  37829  relexpaddss  37836  cotrcltrcl  37843  corcltrcl  37857  cotrclrcl  37860  frege131d  37882  rp-imass  37891  0he  37902  uzmptshftfval  38371  binomcxplemdvbinom  38378  binomcxplemdvsum  38380  binomcxplemnotnn0  38381  rabexgf  39009  uzct  39058  disjf1o  39200  dmresss  39258  dmmptssf  39260  mptssid  39272  fz1ssfz0  39343  uzfissfz  39361  ssuzfz  39384  uzssre2  39452  uzublem  39476  uzssz2  39504  limcperiod  39666  sumnnodd  39668  climconstmpt  39696  fnlimfvre  39712  fnlimabslt  39717  limsupvaluz  39746  limsupubuzlem  39750  limsupubuz  39751  limsupequzmpt2  39756  limsupmnfuzlem  39764  limsupre3uzlem  39773  liminfequzmpt2  39823  cncfshift  39856  cncfperiod  39861  ibliooicc  39956  stoweidlem26  40012  stoweidlem44  40030  stoweidlem50  40036  stoweidlem51  40037  stoweidlem52  40038  stoweidlem57  40043  stoweidlem59  40045  fourierdlem16  40109  fourierdlem19  40112  fourierdlem21  40114  fourierdlem22  40115  fourierdlem42  40135  fourierdlem83  40175  fouriersw  40217  salexct  40321  salexct3  40329  salgencntex  40330  salgensscntex  40331  sge0less  40378  sge0fodjrnlem  40402  sge0isum  40413  ovnsslelem  40543  ovnlerp  40545  ovn0lem  40548  hoidmv1lelem1  40574  hoidmv1lelem3  40576  hoidmvlelem1  40578  hoidmvlelem2  40579  hoidmvlelem3  40580  hoidmvlelem4  40581  ovnhoilem1  40584  ovnhoilem2  40585  opnvonmbllem2  40616  ovolval4lem1  40632  ovolval5lem3  40637  pimdecfgtioc  40694  pimincfltioc  40695  pimdecfgtioo  40696  pimincfltioo  40697  incsmflem  40719  decsmflem  40743  smflimlem2  40749  smflimlem3  40750  smflim  40754  smfrec  40765  smfmullem4  40770  smfdiv  40773  smfsuplem1  40786  smfsuplem3  40788  smfsupxr  40791  smfliminflem  40805  oddibas  41584  2zlidl  41705  2zrngbas  41707  2zrng0  41709  fldc  41854  fldhmsubc  41855  fldcALTV  41872  fldhmsubcALTV  41873  setrec2lem1  42211
  Copyright terms: Public domain W3C validator