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

Theorem eqsstri 3597
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 3591 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 219 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  eqsstr3i  3598  ssrab2  3649  rabssab  3651  opabss  4640  brab2ga  5106  relopabi  5155  dmopabss  5244  resss  5328  relres  5332  rnin  5446  rnxpss  5470  cnvcnvss  5492  dmmptss  5533  predss  5589  fnres  5906  f0  5983  nfvres  6118  fvopab4ndm  6199  ffvresb  6285  funiunfv  6387  isoini2  6466  ovssunirn  6556  dmoprabss  6617  mpt2ndm0  6750  elmpt2cl  6751  omsson  6938  exse2  6975  fabexg  6992  frxp  7151  tposssxp  7220  dftpos4  7235  wfrdmss  7285  smores  7313  smores2  7315  iordsmo  7318  oawordeulem  7498  swoer  7636  swoord1  7637  swoord2  7638  ecss  7652  ecopovsym  7713  ecopovtrn  7714  ecopover  7715  ecopoverOLD  7716  sbthlem7  7938  nnfi  8015  imafi  8119  elfiun  8196  marypha1lem  8199  marypha2lem1  8201  ordtypelem2  8284  hartogslem1  8307  wemapso2lem  8317  wdomima2g  8351  inf3lem1  8385  wemapwe  8454  tc2  8478  tz9.12lem1  8510  rankuni  8586  rankuniss  8589  rankmapu  8601  cplem1  8612  hta  8620  r0weon  8695  infxpenlem  8696  ackbij1lem9  8910  ackbij1lem10  8911  ackbij1b  8921  cofsmo  8951  sdom2en01  8984  fin23lem26  9007  fin23lem28  9022  fin23lem30  9024  isf32lem5  9039  isf32lem6  9040  isf32lem7  9041  isf32lem8  9042  fin56  9075  fin1a2lem9  9090  hsmexlem4  9111  hsmexlem5  9112  hsmexlem6  9113  axdc3lem  9132  axdc3lem2  9133  axcclem  9139  zorn2lem1  9178  zorn2lem3  9180  zorn2lem4  9181  zorn2lem5  9182  imadomg  9214  iundom2g  9218  smobeth  9264  canth4  9325  gruina  9496  grur1a  9497  pinn  9556  niex  9559  ltsopi  9566  ltrelpi  9567  dmaddpi  9568  dmmulpi  9569  enqex  9600  0nnq  9602  elpqn  9603  ltrelnq  9604  nqerf  9608  nqerrel  9610  dmrecnq  9646  lterpq  9648  ltrelpr  9676  enrex  9744  ltrelsr  9745  dmaddsr  9762  dmmulsr  9763  ltrelre  9811  axaddf  9822  axmulf  9823  ltrelxr  9950  lerelxr  9952  nn0ssre  11145  nn0ssz  11233  uzsupss  11614  rpnnen1lem2  11648  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  rpre  11673  uzsup  12481  fzfi  12590  swrd00  13218  sqrlem3  13781  sqrlem5  13783  cau3  13891  caubnd  13894  limsupgre  14008  rlimpm  14027  rlimclim  14073  isercolllem1  14191  isercolllem2  14192  isercoll  14194  caurcvg  14203  caucvg  14205  iseraltlem2  14209  iseraltlem3  14210  zsum  14244  fsumcvg3  14255  climfsum  14341  ackbijnn  14347  divcnvshft  14374  infcvgaux1i  14376  clim2prod  14407  ntrivcvg  14416  ntrivcvgfvn0  14418  ntrivcvgtail  14419  ntrivcvgmullem  14420  ntrivcvgmul  14421  zprod  14454  dvdszrcl  14774  dvdsflip  14825  divalglem2  14904  divalglem5  14906  divalglem8  14909  gcdcllem3  15009  bezoutlem2  15043  bezoutlem3  15044  maxprmfct  15207  phimullem  15270  eulerthlem2  15273  prmdiveq  15277  prmdivdiv  15278  pclem  15329  infpn2  15403  prmreclem2  15407  prmreclem3  15408  prmreclem5  15410  4sqlem1  15438  4sqlem13  15447  4sqlem14  15448  4sqlem17  15451  4sqlem18  15452  4sqlem19  15453  vdwnnlem3  15487  ramcl2lem  15499  ramtcl  15500  ramtcl2  15501  ramtub  15502  ramub1lem2  15517  structcnvcnv  15654  fvsetsid  15670  strlemor0  15743  strlemor1  15744  strleun  15747  imasdsval2  15947  gsumval1  17048  nmzsubg  17406  nmznsg  17409  conjnmz  17465  conjnmzb  17466  gicer  17489  gicerOLD  17490  gastacl  17513  symgbasfi  17577  mvdco  17636  symgsssg  17658  sylow1lem2  17785  sylow1lem3  17786  sylow1lem4  17787  sylow1lem5  17788  sylow2a  17805  sylow3lem2  17814  efglem  17900  efgtf  17906  efgtlen  17910  efginvrel2  17911  efginvrel1  17912  efgsfo  17923  efgredlemg  17926  efgredleme  17927  efgredlemd  17928  efgredlemc  17929  efgredlem  17931  efgred  17932  efgrelexlemb  17934  efgcpbllemb  17939  frgpinv  17948  frgpuplem  17956  frgpupf  17957  frgpup1  17959  frgpnabllem2  18048  gsumval3lem1  18077  gsumval3lem2  18078  gsumval3  18079  ablfacrplem  18235  ablfacrp2  18237  ablfac1eu  18243  pgpfaclem1  18251  ablfaclem2  18256  ablfaclem3  18257  lspsolvlem  18911  lbsextlem2  18928  lbsextlem3  18929  lbsextlem4  18930  rrgeq0  19059  rrgss  19061  psrbagconf1o  19143  psrass1lem  19146  mplbasss  19201  ply1bascl  19342  coe1mul2lem2  19407  znf1o  19666  zntoslem  19671  cygznlem2a  19682  psgnghm  19692  pjpm  19818  dsmmbase  19845  frlmsslsp  19901  mretopd  20653  ordtbas  20753  leordtval2  20773  lecldbas  20780  lmfval  20793  lmbrf  20821  cnconst2  20844  hauscmplem  20966  concompcld  20994  hauspwdom  21061  txuni2  21125  xkouni  21159  xkoccn  21179  txkgen  21212  qtoptop2  21259  kqdisj  21292  hmphtop  21338  hmpher  21344  uzrest  21458  uzfbas  21459  lmflf  21566  ptcmplem1  21613  ptcmplem3  21615  tgpconcompeqg  21672  tgpconcomp  21673  ustn0  21781  imasdsf1olem  21935  xmeter  21995  blcld  22067  isngp2  22158  xrtgioo  22364  iccntr  22379  icccmplem1  22380  icccmplem2  22381  icccmplem3  22382  xmetdcn  22396  metdcn  22398  metdscn2  22415  icchmeo  22495  cnheiborlem  22508  lmmbrf  22812  iscau4  22829  iscauf  22830  caucfil  22833  lmclimf  22854  rrxf  22936  ivthlem1  22971  ivthlem2  22972  ivthlem3  22973  ovolsslem  23003  ovolicc2lem3  23038  ovolicc2lem4  23039  ovolicc2lem5  23040  ovolicc2  23041  volf  23048  uniioombllem3  23103  uniioombllem4  23104  uniioombllem5  23105  dyadmbllem  23117  dyadmbl  23118  volcn  23124  mbfimaopnlem  23172  mbflimsup  23183  i1f1  23207  itg2lcl  23244  iblmbf  23284  itgioo  23332  itgsplitioo  23354  limcflflem  23394  limcflf  23395  limcresi  23399  lhop  23527  dvfsumlem1  23537  dvfsumlem2  23538  dvfsumlem3  23539  dvfsumlem4  23540  dvfsumrlimge0  23541  dvfsumrlim  23542  dvfsumrlim2  23543  dvfsum2  23545  vieta1lem1  23813  vieta1lem2  23814  psercnlem2  23926  psercnlem1  23927  psercn  23928  pserdvlem1  23929  pserdvlem2  23930  pserdv  23931  pserdv2  23932  abelthlem4  23936  abelthlem6  23938  abelthlem9  23942  abelth  23943  logcnlem5  24136  dvlog  24141  dvlog2lem  24142  dvlog2  24143  dvcncxp1  24228  dvcnsqrt  24229  cxpcn3lem  24232  cxpcn3  24233  sqrtcn  24235  1cubr  24313  atansssdm  24404  atancn  24407  jensen  24459  lgamucov  24508  lgamucov2  24509  wilthlem1  24538  ftalem3  24545  musum  24661  dvdsmulf1o  24664  fsumdvdsmul  24665  ppiub  24673  lgsfcl2  24772  lgsquadlem1  24849  lgsquadlem2  24850  lgsquadlem3  24851  2sqlem7  24893  rpvmasum2  24945  dchrisum0re  24946  dchrisum0lema  24947  dchrisum0lem1b  24948  dchrisum0lem1  24949  dchrisum0lem2a  24950  dchrisum0lem2  24951  dchrisum0lem3  24952  dchrisum0  24953  pntlem3  25042  axtgcgrrflx  25105  axtgcgrid  25106  axtgsegcon  25107  axtg5seg  25108  axtgbtwnid  25109  axtgpasch  25110  axtgcont1  25111  tglng  25186  axcontlem2  25590  axcontlem7  25595  axcontlem8  25596  axcontlem10  25598  nbgraf1olem1  25763  disjxwwlkn  26066  clwlknclwlkdifnum  26281  frgrawopreg1  26370  frgrawopreg2  26371  phnv  26846  htthlem  26951  hlimadd  27227  hlimcaui  27270  hhsscms  27313  occllem  27339  shjshsi  27528  3oalem4  27701  pjfi  27740  dmadjss  27923  nlelshi  28096  nlelchi  28097  hmopidmchi  28187  atssch  28379  shatomistici  28397  fcoinver  28591  mptexgf  28602  mptctf  28676  fcobijfs  28682  psgnfzto1stlem  28974  cnre2csqima  29078  raddcn  29096  rrhre  29186  esumsnf  29246  sxbrsiga  29472  omssubadd  29482  carsggect  29500  sitmcl  29533  oddpwdc  29536  eulerpartlem1  29549  eulerpartlemt  29553  eulerpartgbij  29554  eulerpartlemmf  29557  eulerpartlemgvv  29558  eulerpartlemgh  29560  sseqf  29574  ballotlemfmpn  29676  ballotth  29719  signswch  29757  bnj21  29830  bnj1146  29909  bnj1292  29933  bnj1293  29934  bnj1145  30108  bnj1177  30121  subfacp1lem3  30211  subfacp1lem5  30213  erdszelem2  30221  kur14lem3  30237  kur14lem6  30240  kur14lem7  30241  kur14lem9  30243  cvmlift2lem12  30343  mpstssv  30483  mstapst  30491  mppspstlem  30515  mppspst  30518  mthmsta  30522  mthmpps  30526  mclsppslem  30527  dfpo2  30691  wlimss  30815  frrlem7  30827  txpss3v  30948  pprodss4v  30954  relsset  30958  fixssdm  30976  fixssrn  30977  limitssson  30981  funpartss  31014  colinearex  31130  fneer  31311  neibastop1  31317  neibastop2lem  31318  filnetlem2  31337  filnetlem3  31338  knoppcnlem10  31455  bj-tagss  31944  bj-dmtopon  32025  bj-cmnssmnd  32096  bj-ablssgrp  32098  bj-ablsscmn  32100  bj-vecssmod  32103  bj-rrvecssvec  32110  icoreresf  32159  icoreunrn  32166  poimirlem29  32391  poimirlem30  32392  poimirlem31  32393  poimir  32395  broucube  32396  dvasin  32449  dvacos  32450  areacirc  32458  caures  32509  bnd2lem  32543  ismtyres  32560  flddivrng  32751  toycom  33061  dihglblem2N  35384  lcdvbase  35683  mapdunirnN  35740  eldiophb  36121  monotuz  36307  fglmod  36444  pwssplit4  36460  pwfi2f1o  36467  arearect  36603  fvnonrel  36705  rclexi  36724  rtrclex  36726  trclexi  36729  rtrclexi  36730  clcnvlem  36732  cnvrcl0  36734  cnvtrcl0  36735  dfrtrcl5  36738  dfrcl2  36768  comptiunov2i  36800  corclrcl  36801  trclrelexplem  36805  relexpaddss  36812  cotrcltrcl  36819  corcltrcl  36833  cotrclrcl  36836  frege131d  36858  rp-imass  36868  0he  36879  uzmptshftfval  37350  binomcxplemdvbinom  37357  binomcxplemdvsum  37359  binomcxplemnotnn0  37360  rabexgf  37989  uzct  38040  disjf1o  38156  fz1ssfz0  38248  uzfissfz  38266  ssuzfz  38289  limcperiod  38478  sumnnodd  38480  climconstmpt  38508  fnlimfvre  38524  fnlimabslt  38529  cncfshift  38542  cncfperiod  38547  ibliooicc  38646  stoweidlem26  38702  stoweidlem44  38720  stoweidlem50  38726  stoweidlem51  38727  stoweidlem52  38728  stoweidlem57  38733  stoweidlem59  38735  fourierdlem16  38799  fourierdlem19  38802  fourierdlem21  38804  fourierdlem22  38805  fourierdlem42  38825  fourierdlem83  38865  fouriersw  38907  salexct  39011  salexct3  39019  salgencntex  39020  salgensscntex  39021  sge0less  39068  sge0fodjrnlem  39092  sge0isum  39103  ovnsslelem  39233  ovnlerp  39235  ovn0lem  39238  hoidmv1lelem1  39264  hoidmv1lelem3  39266  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  ovnhoilem1  39274  ovnhoilem2  39275  opnvonmbllem2  39306  ovolval4lem1  39322  ovolval5lem3  39327  pimdecfgtioc  39385  pimincfltioc  39386  pimdecfgtioo  39387  pimincfltioo  39388  incsmflem  39411  decsmflem  39435  smflimlem2  39441  smflimlem3  39442  smflim  39446  smfrec  39457  smfmullem4  39462  smfdiv  39465  av-disjxwwlkn  41100  clwwlknclwwlkdifnum  41163  clwwlkssswrd  41199  frgrwopreg1  41468  frgrwopreg2  41469  oddibas  41584  2zlidl  41705  2zrngbas  41707  2zrng0  41709  fldc  41856  fldhmsubc  41857  fldcALTV  41875  fldhmsubcALTV  41876
  Copyright terms: Public domain W3C validator