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

Theorem eqsstri 4000
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 3994 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 232 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  eqsstrri  4001  ssrab2  4055  ssrab3  4056  rabssab  4059  opabss  5122  brab2a  5638  relopabiALT  5689  dmopabss  5781  resss  5872  relres  5876  rnin  5999  rnxpss  6023  cnvcnvss  6045  predss  6149  fnres  6468  f0  6554  nfvres  6700  fvopab4ndm  6790  ffvresb  6881  mptexgf  6977  funiunfv  6998  isoini2  7081  ovssunirn  7181  dmoprabss  7245  mpondm0  7375  elmpocl  7376  exse2  7610  fabexg  7627  frxp  7811  tposssxp  7887  dftpos4  7902  wfrdmss  7952  smores  7980  smores2  7982  iordsmo  7985  swoer  8309  swoord1  8310  swoord2  8311  ecss  8325  ecopovsym  8389  ecopovtrn  8390  ecopover  8391  sbthlem7  8622  nnfi  8700  imafi  8806  elfiun  8883  marypha1lem  8886  marypha2lem1  8888  hartogslem1  8995  wdomima2g  9039  inf3lem1  9080  tc2  9173  tz9.12lem1  9205  rankuni  9281  rankuniss  9284  rankmapu  9296  hta  9315  r0weon  9427  infxpenlem  9428  ackbij1lem9  9639  ackbij1lem10  9640  ackbij1b  9650  sdom2en01  9713  fin23lem26  9736  fin56  9804  fin1a2lem9  9819  axdc3lem  9861  axdc3lem2  9862  axcclem  9868  imadomg  9945  iundom2g  9951  smobeth  9997  canth4  10058  gruina  10229  grur1a  10230  pinn  10289  niex  10292  ltsopi  10299  ltrelpi  10300  dmaddpi  10301  dmmulpi  10302  enqex  10333  ltrelnq  10337  nqerf  10341  nqerrel  10343  dmrecnq  10379  lterpq  10381  ltrelpr  10409  enrex  10478  ltrelsr  10479  dmaddsr  10496  dmmulsr  10497  ltrelre  10545  axaddf  10556  axmulf  10557  ltrelxr  10691  lerelxr  10693  nn0ssre  11890  nn0sscn  11891  nn0ssz  11992  uzsupss  12329  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  fz1ssfz0  12993  uzsup  13221  fzfi  13330  swrd00  13996  sqrlem3  14594  cau3  14705  caubnd  14708  limsupgre  14828  rlimpm  14847  rlimclim  14893  isercolllem1  15011  isercolllem2  15012  isercoll  15014  caurcvg  15023  caucvg  15025  iseraltlem2  15029  iseraltlem3  15030  zsum  15065  fsumcvg3  15076  climfsum  15165  ackbijnn  15173  divcnvshft  15200  infcvgaux1i  15202  clim2prod  15234  ntrivcvg  15243  ntrivcvgfvn0  15245  ntrivcvgtail  15246  ntrivcvgmullem  15247  ntrivcvgmul  15248  zprod  15281  dvdszrcl  15602  4sqlem1  16274  4sqlem19  16289  ramub1lem2  16353  structcnvcnv  16487  fvsetsid  16505  strleun  16581  gicer  18356  symgbasfi  18444  mvdco  18504  symgsssg  18526  efglem  18773  efgtf  18779  efgtlen  18783  efginvrel2  18784  efginvrel1  18785  efgsfo  18796  efgredlemg  18799  efgredleme  18800  efgredlemd  18801  efgredlemc  18802  efgredlem  18804  efgred  18805  efgrelexlemb  18807  efgcpbllemb  18812  frgpinv  18821  frgpuplem  18829  frgpupf  18830  frgpup1  18832  frgpnabllem2  18925  gsumval3lem1  18956  gsumval3lem2  18957  gsumval3  18958  lbsextlem3  19863  ply1bascl  20301  znf1o  20628  zntoslem  20633  pjpm  20782  dmtopon  21461  ordtbas  21730  leordtval2  21750  lecldbas  21757  lmfval  21770  lmbrf  21798  cnconst2  21821  conncompcld  21972  hauspwdom  22039  txuni2  22103  xkouni  22137  xkoccn  22157  txkgen  22190  qtoptop2  22237  kqdisj  22270  hmphtop  22316  hmpher  22322  uzrest  22435  uzfbas  22436  lmflf  22543  tgpconncompeqg  22649  tgpconncomp  22650  ustn0  22758  xmeter  22972  isngp2  23135  xrtgioo  23343  iccntr  23358  xmetdcn  23375  metdcn  23377  metdscn2  23394  icchmeo  23474  cnheiborlem  23487  lmmbrf  23794  iscau4  23811  iscauf  23812  caucfil  23815  lmclimf  23836  volf  24059  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  volcn  24136  mbfimaopnlem  24185  mbflimsup  24196  i1f1  24220  itg2lcl  24257  itgioo  24345  itgsplitioo  24367  limcflflem  24407  limcflf  24408  limcresi  24412  lhop  24542  dvfsumlem1  24552  dvfsumlem2  24553  dvfsumlem3  24554  dvfsumlem4  24555  dvfsumrlimge0  24556  dvfsumrlim  24557  dvfsumrlim2  24558  dvfsum2  24560  vieta1lem1  24828  vieta1lem2  24829  psercnlem2  24941  psercnlem1  24942  psercn  24943  pserdvlem1  24944  pserdvlem2  24945  pserdv  24946  pserdv2  24947  logcnlem5  25156  dvlog  25161  dvlog2lem  25162  dvlog2  25163  dvcncxp1  25251  dvcnsqrt  25252  cxpcn3lem  25255  cxpcn3  25256  sqrtcn  25258  1cubr  25347  atansssdm  25438  jensen  25494  musum  25696  ppiub  25708  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  2sqlem7  25928  axtgcgrrflx  26176  axtgcgrid  26177  axtgsegcon  26178  axtg5seg  26179  axtgbtwnid  26180  axtgpasch  26181  axtgcont1  26182  tglng  26260  disjxwwlkn  27620  frgrwopreg2  28026  phnv  28519  htthlem  28622  hlimadd  28898  hlimcaui  28941  hhsscms  28983  occllem  29008  shjshsi  29197  3oalem4  29370  pjfi  29409  dmadjss  29592  nlelshi  29765  nlelchi  29766  hmopidmchi  29856  shatomistici  30066  difxp1ss  30210  difxp2ss  30211  fcoinver  30286  opabssi  30293  mptctf  30380  fcobijfs  30386  pmtrcnel2  30662  psgnfzto1stlem  30670  cycpmrn  30713  cyc3genpm  30722  cnre2csqima  31054  raddcn  31072  rrhre  31162  esumsnf  31223  sxbrsiga  31448  omssubadd  31458  carsggect  31476  sitmcl  31509  oddpwdc  31512  eulerpartlem1  31525  eulerpartlemt  31529  eulerpartgbij  31530  eulerpartlemmf  31533  eulerpartlemgh  31536  sseqf  31550  ballotlemfmpn  31652  ballotth  31695  signswch  31731  ftc2re  31769  fdvposlt  31770  fdvposle  31772  bnj1146  31963  bnj1292  31987  bnj1293  31988  bnj1145  32163  bnj1177  32176  subfacp1lem3  32327  subfacp1lem5  32329  erdszelem2  32337  kur14lem3  32353  kur14lem6  32356  kur14lem7  32357  kur14lem9  32359  cvmlift2lem12  32459  mpstssv  32684  mstapst  32692  mppspstlem  32716  mppspst  32719  mthmsta  32723  mthmpps  32727  mclsppslem  32728  dfpo2  32889  nosupbnd1lem1  33106  nosupbnd2  33114  scutf  33171  txpss3v  33237  pprodss4v  33243  relsset  33247  fixssdm  33265  fixssrn  33266  limitssson  33270  funpartss  33303  colinearex  33419  fneer  33599  neibastop1  33605  neibastop2lem  33606  filnetlem2  33625  filnetlem3  33626  knoppcnlem10  33739  bj-tagss  34190  bj-fvsnun2  34431  bj-ablssgrp  34447  bj-ablsscmn  34449  bj-vecssmod  34452  bj-flddrng  34459  icoreresf  34516  icoreunrn  34523  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimir  34807  broucube  34808  dvasin  34860  dvacos  34861  areacirc  34869  caures  34918  bnd2lem  34952  ismtyres  34969  flddivrng  35160  xrnss3v  35506  refrelsredund2  35750  toycom  35991  dihglblem2N  38312  lcdvbase  38611  mapdunirnN  38668  prjspreln0  39139  prjspvs  39140  prjspeclsp  39142  0prjspnrel  39149  dffltz  39151  eldiophb  39234  monotuz  39418  pwssplit4  39569  pwfi2f1o  39576  arearect  39702  fvnonrel  39837  rclexi  39855  rtrclex  39857  trclexi  39860  rtrclexi  39861  clcnvlem  39863  cnvrcl0  39865  cnvtrcl0  39866  dfrtrcl5  39869  dfrcl2  39899  comptiunov2i  39931  corclrcl  39932  trclrelexplem  39936  relexpaddss  39943  cotrcltrcl  39950  corcltrcl  39964  cotrclrcl  39967  frege131d  39989  rp-imass  39997  0he  40008  grumnudlem  40501  uzmptshftfval  40558  binomcxplemdvbinom  40565  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  rabexgf  41161  uzct  41205  disjf1o  41332  dmresss  41381  dmmptssf  41382  mptssid  41391  uzfissfz  41474  ssuzfz  41497  uzssre2  41560  uzublem  41584  uzssz2  41612  uzsscn2  41634  sumnnodd  41791  climconstmpt  41819  fnlimfvre  41835  fnlimabslt  41840  limsupvaluz  41869  limsupubuzlem  41873  limsupubuz  41874  limsupequzmpt2  41879  limsupmnfuzlem  41887  limsupre3uzlem  41896  liminfequzmpt2  41952  ibliooicc  42136  stoweidlem44  42210  stoweidlem50  42216  stoweidlem51  42217  stoweidlem52  42218  stoweidlem57  42223  stoweidlem59  42225  fourierdlem16  42289  fourierdlem19  42292  fourierdlem21  42294  fourierdlem22  42295  fourierdlem42  42315  fourierdlem83  42355  fouriersw  42397  salexct  42498  salexct3  42506  salgencntex  42507  salgensscntex  42508  sge0less  42555  sge0fodjrnlem  42579  sge0isum  42590  ovnsslelem  42723  ovnlerp  42725  ovn0lem  42728  hoidmv1lelem1  42754  hoidmv1lelem3  42756  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvlelem4  42761  ovnhoilem1  42764  ovnhoilem2  42765  opnvonmbllem2  42796  ovolval4lem1  42812  ovolval5lem3  42817  pimdecfgtioc  42874  pimincfltioc  42875  pimdecfgtioo  42876  pimincfltioo  42877  incsmflem  42899  decsmflem  42923  smflimlem2  42929  smflimlem3  42930  smflim  42934  smfrec  42945  smfmullem4  42950  smfdiv  42953  smfsuplem1  42966  smfsuplem3  42968  smfsupxr  42971  smfliminflem  42985  oddibas  43927  smndex1sgrp  43978  2zlidl  44103  2zrngbas  44105  2zrng0  44107  fldc  44252  fldhmsubc  44253  fldcALTV  44270  fldhmsubcALTV  44271  setrec2lem1  44694
  Copyright terms: Public domain W3C validator