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

Theorem eqsstri 3782
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 3776 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 221 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  wss 3721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-in 3728  df-ss 3735
This theorem is referenced by:  eqsstr3i  3783  ssrab2  3834  ssrab3  3835  rabssab  3838  opabss  4846  brab2a  5334  relopabiALT  5385  dmopabss  5474  resss  5563  relres  5567  rnin  5683  rnxpss  5707  cnvcnvss  5730  dmmptss  5775  predss  5830  fnres  6147  f0  6226  nfvres  6365  fvopab4ndm  6449  ffvresb  6536  mptexgf  6628  funiunfv  6648  isoini2  6731  ovssunirn  6825  dmoprabss  6888  mpt2ndm0  7021  elmpt2cl  7022  omsson  7215  exse2  7251  fabexg  7268  frxp  7437  tposssxp  7507  dftpos4  7522  wfrdmss  7573  smores  7601  smores2  7603  iordsmo  7606  oawordeulem  7787  swoer  7925  swoord1  7926  swoord2  7927  ecss  7939  ecopovsym  8001  ecopovtrn  8002  ecopover  8003  sbthlem7  8231  nnfi  8308  imafi  8414  elfiun  8491  marypha1lem  8494  marypha2lem1  8496  ordtypelem2  8579  hartogslem1  8602  wemapso2lem  8612  wdomima2g  8646  inf3lem1  8688  wemapwe  8757  tc2  8781  tz9.12lem1  8813  rankuni  8889  rankuniss  8892  rankmapu  8904  cplem1  8915  hta  8923  r0weon  9034  infxpenlem  9035  ackbij1lem9  9251  ackbij1lem10  9252  ackbij1b  9262  cofsmo  9292  sdom2en01  9325  fin23lem26  9348  fin23lem28  9363  fin23lem30  9365  isf32lem5  9380  isf32lem6  9381  isf32lem7  9382  isf32lem8  9383  fin56  9416  fin1a2lem9  9431  hsmexlem4  9452  hsmexlem5  9453  hsmexlem6  9454  axdc3lem  9473  axdc3lem2  9474  axcclem  9480  zorn2lem1  9519  zorn2lem3  9521  zorn2lem4  9522  zorn2lem5  9523  imadomg  9557  iundom2g  9563  smobeth  9609  canth4  9670  gruina  9841  grur1a  9842  pinn  9901  niex  9904  ltsopi  9911  ltrelpi  9912  dmaddpi  9913  dmmulpi  9914  enqex  9945  0nnq  9947  elpqn  9948  ltrelnq  9949  nqerf  9953  nqerrel  9955  dmrecnq  9991  lterpq  9993  ltrelpr  10021  enrex  10089  ltrelsr  10090  dmaddsr  10107  dmmulsr  10108  ltrelre  10156  axaddf  10167  axmulf  10168  ltrelxr  10300  lerelxr  10302  nn0ssre  11497  nn0ssz  11599  uzsupss  11982  rpnnen1lem2  12016  rpnnen1lem1  12017  rpnnen1lem3  12018  rpnnen1lem5  12020  rpnnen1lem1OLD  12023  rpnnen1lem3OLD  12024  rpnnen1lem5OLD  12026  rpre  12041  fz1ssfz0  12642  uzsup  12869  fzfi  12978  swrd00  13625  sqrlem3  14192  sqrlem5  14194  cau3  14302  caubnd  14305  limsupgre  14419  rlimpm  14438  rlimclim  14484  isercolllem1  14602  isercolllem2  14603  isercoll  14605  caurcvg  14614  caucvg  14616  iseraltlem2  14620  iseraltlem3  14621  zsum  14656  fsumcvg3  14667  climfsum  14758  ackbijnn  14766  divcnvshft  14793  infcvgaux1i  14795  clim2prod  14826  ntrivcvg  14835  ntrivcvgfvn0  14837  ntrivcvgtail  14838  ntrivcvgmullem  14839  ntrivcvgmul  14840  zprod  14873  dvdszrcl  15193  dvdsflip  15247  divalglem2  15325  divalglem5  15327  divalglem8  15330  gcdcllem3  15430  bezoutlem2  15464  bezoutlem3  15465  maxprmfct  15627  phimullem  15690  eulerthlem2  15693  pclem  15749  infpn2  15823  prmreclem2  15827  prmreclem3  15828  prmreclem5  15830  4sqlem1  15858  4sqlem13  15867  4sqlem14  15868  4sqlem17  15871  4sqlem18  15872  4sqlem19  15873  vdwnnlem3  15907  ramcl2lem  15919  ramtcl  15920  ramtcl2  15921  ramtub  15922  ramub1lem2  15937  structcnvcnv  16077  fvsetsid  16096  strlemor0OLD  16175  strlemor1OLD  16176  strleun  16179  imasdsval2  16383  gsumval1  17484  nmzsubg  17842  nmznsg  17845  conjnmz  17901  conjnmzb  17902  gicer  17925  gastacl  17948  symgbasfi  18012  mvdco  18071  symgsssg  18093  sylow1lem2  18220  sylow1lem3  18221  sylow1lem4  18222  sylow1lem5  18223  sylow2a  18240  sylow3lem2  18249  efglem  18335  efgtf  18341  efgtlen  18345  efginvrel2  18346  efginvrel1  18347  efgsfo  18358  efgredlemg  18361  efgredleme  18362  efgredlemd  18363  efgredlemc  18364  efgredlem  18366  efgred  18367  efgrelexlemb  18369  efgcpbllemb  18374  frgpinv  18383  frgpuplem  18391  frgpupf  18392  frgpup1  18394  frgpnabllem2  18483  gsumval3lem1  18512  gsumval3lem2  18513  gsumval3  18514  ablfacrplem  18671  ablfacrp2  18673  ablfac1eu  18679  pgpfaclem1  18687  ablfaclem2  18692  ablfaclem3  18693  lspsolvlem  19355  lbsextlem2  19373  lbsextlem3  19374  lbsextlem4  19375  rrgeq0  19504  rrgss  19506  psrbagconf1o  19588  psrass1lem  19591  mplbasss  19646  ply1bascl  19787  coe1mul2lem2  19852  znf1o  20114  zntoslem  20119  cygznlem2a  20130  psgnghm  20140  pjpm  20268  dsmmbase  20295  frlmsslsp  20351  dmtopon  20947  mretopd  21116  ordtbas  21216  leordtval2  21236  lecldbas  21243  lmfval  21256  lmbrf  21284  cnconst2  21307  hauscmplem  21429  conncompcld  21457  hauspwdom  21524  txuni2  21588  xkouni  21622  xkoccn  21642  txkgen  21675  qtoptop2  21722  kqdisj  21755  hmphtop  21801  hmpher  21807  uzrest  21920  uzfbas  21921  lmflf  22028  ptcmplem1  22075  ptcmplem3  22077  tgpconncompeqg  22134  tgpconncomp  22135  ustn0  22243  imasdsf1olem  22397  xmeter  22457  blcld  22529  isngp2  22620  xrtgioo  22828  iccntr  22843  icccmplem1  22844  icccmplem2  22845  icccmplem3  22846  xmetdcn  22860  metdcn  22862  metdscn2  22879  icchmeo  22959  cnheiborlem  22972  lmmbrf  23278  iscau4  23295  iscauf  23296  caucfil  23299  lmclimf  23320  rrxf  23402  ivthlem1  23438  ivthlem2  23439  ivthlem3  23440  ovolsslem  23471  ovolicc2lem3  23506  ovolicc2lem4  23507  ovolicc2lem5  23508  ovolicc2  23509  volf  23516  uniioombllem3  23572  uniioombllem4  23573  uniioombllem5  23574  dyadmbllem  23586  dyadmbl  23587  volcn  23593  mbfimaopnlem  23641  mbflimsup  23652  i1f1  23676  itg2lcl  23713  iblmbf  23753  itgioo  23801  itgsplitioo  23823  limcflflem  23863  limcflf  23864  limcresi  23868  lhop  23998  dvfsumlem1  24008  dvfsumlem2  24009  dvfsumlem3  24010  dvfsumlem4  24011  dvfsumrlimge0  24012  dvfsumrlim  24013  dvfsumrlim2  24014  dvfsum2  24016  vieta1lem1  24284  vieta1lem2  24285  psercnlem2  24397  psercnlem1  24398  psercn  24399  pserdvlem1  24400  pserdvlem2  24401  pserdv  24402  pserdv2  24403  abelthlem4  24407  abelthlem6  24409  abelthlem9  24413  abelth  24414  logcnlem5  24612  dvlog  24617  dvlog2lem  24618  dvlog2  24619  dvcncxp1  24704  dvcnsqrt  24705  cxpcn3lem  24708  cxpcn3  24709  sqrtcn  24711  1cubr  24789  atansssdm  24880  atancn  24883  jensen  24935  lgamucov  24984  lgamucov2  24985  ftalem3  25021  musum  25137  dvdsmulf1o  25140  fsumdvdsmul  25141  ppiub  25149  lgsfcl2  25248  lgsquadlem1  25325  lgsquadlem2  25326  lgsquadlem3  25327  2sqlem7  25369  rpvmasum2  25421  dchrisum0re  25422  dchrisum0lema  25423  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0lem3  25428  dchrisum0  25429  pntlem3  25518  axtgcgrrflx  25581  axtgcgrid  25582  axtgsegcon  25583  axtg5seg  25584  axtgbtwnid  25585  axtgpasch  25586  axtgcont1  25587  tglng  25661  axcontlem2  26065  axcontlem7  26070  axcontlem8  26071  axcontlem10  26073  upgrreslem  26418  umgrreslem  26419  vtxdginducedm1lem2  26670  finsumvtxdg2ssteplem1  26675  disjxwwlkn  27055  clwwlknclwwlkdifnumOLD  27127  clwwlksswrd  27134  frgrwopreg2  27498  dlwwlknonclwlknonf1olem2  27550  phnv  28003  htthlem  28108  hlimadd  28384  hlimcaui  28427  hhsscms  28470  occllem  28496  shjshsi  28685  3oalem4  28858  pjfi  28897  dmadjss  29080  nlelshi  29253  nlelchi  29254  hmopidmchi  29344  atssch  29536  shatomistici  29554  fcoinver  29750  opabssi  29757  mptctf  29829  fcobijfs  29835  psgnfzto1stlem  30184  cnre2csqima  30291  raddcn  30309  rrhre  30399  esumsnf  30460  sxbrsiga  30686  omssubadd  30696  carsggect  30714  sitmcl  30747  oddpwdc  30750  eulerpartlem1  30763  eulerpartlemt  30767  eulerpartgbij  30768  eulerpartlemmf  30771  eulerpartlemgh  30774  sseqf  30788  ballotlemfmpn  30890  ballotth  30933  signswch  30972  ftc2re  31010  fdvposlt  31011  fdvposle  31013  bnj1146  31194  bnj1292  31218  bnj1293  31219  bnj1145  31393  bnj1177  31406  subfacp1lem3  31496  subfacp1lem5  31498  erdszelem2  31506  kur14lem3  31522  kur14lem6  31525  kur14lem7  31526  kur14lem9  31528  cvmlift2lem12  31628  mpstssv  31768  mstapst  31776  mppspstlem  31800  mppspst  31803  mthmsta  31807  mthmpps  31811  mclsppslem  31812  dfpo2  31977  wlimss  32105  frrlem7  32121  nosupbnd1lem1  32185  nosupbnd2  32193  scutf  32250  txpss3v  32316  pprodss4v  32322  relsset  32326  fixssdm  32344  fixssrn  32345  limitssson  32349  funpartss  32382  colinearex  32498  fneer  32679  neibastop1  32685  neibastop2lem  32686  filnetlem2  32705  filnetlem3  32706  knoppcnlem10  32823  bj-tagss  33293  bj-cmnssmnd  33466  bj-ablssgrp  33468  bj-ablsscmn  33470  bj-vecssmod  33473  bj-rrvecssvec  33480  icoreresf  33530  icoreunrn  33537  cnfinltrel  33571  poimirlem29  33764  poimirlem30  33765  poimirlem31  33766  poimir  33768  broucube  33769  dvasin  33821  dvacos  33822  areacirc  33830  caures  33881  bnd2lem  33915  ismtyres  33932  flddivrng  34123  xrnss3v  34469  toycom  34775  dihglblem2N  37097  lcdvbase  37396  mapdunirnN  37453  eldiophb  37839  monotuz  38025  fglmod  38162  pwssplit4  38178  pwfi2f1o  38185  arearect  38320  fvnonrel  38422  rclexi  38441  rtrclex  38443  trclexi  38446  rtrclexi  38447  clcnvlem  38449  cnvrcl0  38451  cnvtrcl0  38452  dfrtrcl5  38455  dfrcl2  38485  comptiunov2i  38517  corclrcl  38518  trclrelexplem  38522  relexpaddss  38529  cotrcltrcl  38536  corcltrcl  38550  cotrclrcl  38553  frege131d  38575  rp-imass  38584  0he  38595  uzmptshftfval  39064  binomcxplemdvbinom  39071  binomcxplemdvsum  39073  binomcxplemnotnn0  39074  rabexgf  39699  uzct  39747  disjf1o  39892  dmresss  39948  dmmptssf  39950  mptssid  39962  uzfissfz  40052  ssuzfz  40075  uzssre2  40143  uzublem  40167  uzssz2  40195  uzsscn2  40218  limcperiod  40372  sumnnodd  40374  climconstmpt  40402  fnlimfvre  40418  fnlimabslt  40423  limsupvaluz  40452  limsupubuzlem  40456  limsupubuz  40457  limsupequzmpt2  40462  limsupmnfuzlem  40470  limsupre3uzlem  40479  liminfequzmpt2  40535  cncfshift  40599  cncfperiod  40604  ibliooicc  40698  stoweidlem44  40772  stoweidlem50  40778  stoweidlem51  40779  stoweidlem52  40780  stoweidlem57  40785  stoweidlem59  40787  fourierdlem16  40851  fourierdlem19  40854  fourierdlem21  40856  fourierdlem22  40857  fourierdlem42  40877  fourierdlem83  40917  fouriersw  40959  salexct  41063  salexct3  41071  salgencntex  41072  salgensscntex  41073  sge0less  41120  sge0fodjrnlem  41144  sge0isum  41155  ovnsslelem  41288  ovnlerp  41290  ovn0lem  41293  hoidmv1lelem1  41319  hoidmv1lelem3  41321  hoidmvlelem1  41323  hoidmvlelem2  41324  hoidmvlelem3  41325  hoidmvlelem4  41326  ovnhoilem1  41329  ovnhoilem2  41330  opnvonmbllem2  41361  ovolval4lem1  41377  ovolval5lem3  41382  pimdecfgtioc  41439  pimincfltioc  41440  pimdecfgtioo  41441  pimincfltioo  41442  incsmflem  41464  decsmflem  41488  smflimlem2  41494  smflimlem3  41495  smflim  41499  smfrec  41510  smfmullem4  41515  smfdiv  41518  smfsuplem1  41531  smfsuplem3  41533  smfsupxr  41536  smfliminflem  41550  oddibas  42331  2zlidl  42452  2zrngbas  42454  2zrng0  42456  fldc  42601  fldhmsubc  42602  fldcALTV  42619  fldhmsubcALTV  42620  setrec2lem1  42958
  Copyright terms: Public domain W3C validator