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

Theorem eqsstri 3668
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 3662 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 221 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  eqsstr3i  3669  ssrab2  3720  ssrab3  3721  rabssab  3723  opabss  4747  brab2a  5228  relopabiALT  5279  dmopabss  5368  resss  5457  relres  5461  rnin  5577  rnxpss  5601  cnvcnvss  5624  dmmptss  5669  predss  5725  fnres  6045  f0  6124  nfvres  6262  fvopab4ndm  6346  ffvresb  6434  mptexgf  6526  funiunfv  6546  isoini2  6629  ovssunirn  6721  dmoprabss  6784  mpt2ndm0  6917  elmpt2cl  6918  omsson  7111  exse2  7147  fabexg  7164  frxp  7332  tposssxp  7401  dftpos4  7416  wfrdmss  7466  smores  7494  smores2  7496  iordsmo  7499  oawordeulem  7679  swoer  7817  swoord1  7818  swoord2  7819  ecss  7831  ecopovsym  7892  ecopovtrn  7893  ecopover  7894  sbthlem7  8117  nnfi  8194  imafi  8300  elfiun  8377  marypha1lem  8380  marypha2lem1  8382  ordtypelem2  8465  hartogslem1  8488  wemapso2lem  8498  wdomima2g  8532  inf3lem1  8563  wemapwe  8632  tc2  8656  tz9.12lem1  8688  rankuni  8764  rankuniss  8767  rankmapu  8779  cplem1  8790  hta  8798  r0weon  8873  infxpenlem  8874  ackbij1lem9  9088  ackbij1lem10  9089  ackbij1b  9099  cofsmo  9129  sdom2en01  9162  fin23lem26  9185  fin23lem28  9200  fin23lem30  9202  isf32lem5  9217  isf32lem6  9218  isf32lem7  9219  isf32lem8  9220  fin56  9253  fin1a2lem9  9268  hsmexlem4  9289  hsmexlem5  9290  hsmexlem6  9291  axdc3lem  9310  axdc3lem2  9311  axcclem  9317  zorn2lem1  9356  zorn2lem3  9358  zorn2lem4  9359  zorn2lem5  9360  imadomg  9394  iundom2g  9400  smobeth  9446  canth4  9507  gruina  9678  grur1a  9679  pinn  9738  niex  9741  ltsopi  9748  ltrelpi  9749  dmaddpi  9750  dmmulpi  9751  enqex  9782  0nnq  9784  elpqn  9785  ltrelnq  9786  nqerf  9790  nqerrel  9792  dmrecnq  9828  lterpq  9830  ltrelpr  9858  enrex  9926  ltrelsr  9927  dmaddsr  9944  dmmulsr  9945  ltrelre  9993  axaddf  10004  axmulf  10005  ltrelxr  10137  lerelxr  10139  nn0ssre  11334  nn0ssz  11436  uzsupss  11818  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  rpre  11877  fz1ssfz0  12474  uzsup  12702  fzfi  12811  swrd00  13463  sqrlem3  14029  sqrlem5  14031  cau3  14139  caubnd  14142  limsupgre  14256  rlimpm  14275  rlimclim  14321  isercolllem1  14439  isercolllem2  14440  isercoll  14442  caurcvg  14451  caucvg  14453  iseraltlem2  14457  iseraltlem3  14458  zsum  14493  fsumcvg3  14504  climfsum  14596  ackbijnn  14604  divcnvshft  14631  infcvgaux1i  14633  clim2prod  14664  ntrivcvg  14673  ntrivcvgfvn0  14675  ntrivcvgtail  14676  ntrivcvgmullem  14677  ntrivcvgmul  14678  zprod  14711  dvdszrcl  15032  dvdsflip  15086  divalglem2  15165  divalglem5  15167  divalglem8  15170  gcdcllem3  15270  bezoutlem2  15304  bezoutlem3  15305  maxprmfct  15468  phimullem  15531  eulerthlem2  15534  pclem  15590  infpn2  15664  prmreclem2  15668  prmreclem3  15669  prmreclem5  15671  4sqlem1  15699  4sqlem13  15708  4sqlem14  15709  4sqlem17  15712  4sqlem18  15713  4sqlem19  15714  vdwnnlem3  15748  ramcl2lem  15760  ramtcl  15761  ramtcl2  15762  ramtub  15763  ramub1lem2  15778  structcnvcnv  15918  fvsetsid  15937  strlemor0OLD  16015  strlemor1OLD  16016  strleun  16019  imasdsval2  16223  gsumval1  17324  nmzsubg  17682  nmznsg  17685  conjnmz  17741  conjnmzb  17742  gicer  17765  gastacl  17788  symgbasfi  17852  mvdco  17911  symgsssg  17933  sylow1lem2  18060  sylow1lem3  18061  sylow1lem4  18062  sylow1lem5  18063  sylow2a  18080  sylow3lem2  18089  efglem  18175  efgtf  18181  efgtlen  18185  efginvrel2  18186  efginvrel1  18187  efgsfo  18198  efgredlemg  18201  efgredleme  18202  efgredlemd  18203  efgredlemc  18204  efgredlem  18206  efgred  18207  efgrelexlemb  18209  efgcpbllemb  18214  frgpinv  18223  frgpuplem  18231  frgpupf  18232  frgpup1  18234  frgpnabllem2  18323  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  ablfacrplem  18510  ablfacrp2  18512  ablfac1eu  18518  pgpfaclem1  18526  ablfaclem2  18531  ablfaclem3  18532  lspsolvlem  19190  lbsextlem2  19207  lbsextlem3  19208  lbsextlem4  19209  rrgeq0  19338  rrgss  19340  psrbagconf1o  19422  psrass1lem  19425  mplbasss  19480  ply1bascl  19621  coe1mul2lem2  19686  znf1o  19948  zntoslem  19953  cygznlem2a  19964  psgnghm  19974  pjpm  20100  dsmmbase  20127  frlmsslsp  20183  dmtopon  20775  mretopd  20944  ordtbas  21044  leordtval2  21064  lecldbas  21071  lmfval  21084  lmbrf  21112  cnconst2  21135  hauscmplem  21257  conncompcld  21285  hauspwdom  21352  txuni2  21416  xkouni  21450  xkoccn  21470  txkgen  21503  qtoptop2  21550  kqdisj  21583  hmphtop  21629  hmpher  21635  uzrest  21748  uzfbas  21749  lmflf  21856  ptcmplem1  21903  ptcmplem3  21905  tgpconncompeqg  21962  tgpconncomp  21963  ustn0  22071  imasdsf1olem  22225  xmeter  22285  blcld  22357  isngp2  22448  xrtgioo  22656  iccntr  22671  icccmplem1  22672  icccmplem2  22673  icccmplem3  22674  xmetdcn  22688  metdcn  22690  metdscn2  22707  icchmeo  22787  cnheiborlem  22800  lmmbrf  23106  iscau4  23123  iscauf  23124  caucfil  23127  lmclimf  23148  rrxf  23230  ivthlem1  23266  ivthlem2  23267  ivthlem3  23268  ovolsslem  23298  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicc2  23336  volf  23343  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  dyadmbllem  23413  dyadmbl  23414  volcn  23420  mbfimaopnlem  23467  mbflimsup  23478  i1f1  23502  itg2lcl  23539  iblmbf  23579  itgioo  23627  itgsplitioo  23649  limcflflem  23689  limcflf  23690  limcresi  23694  lhop  23824  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlimge0  23838  dvfsumrlim  23839  dvfsumrlim2  23840  dvfsum2  23842  vieta1lem1  24110  vieta1lem2  24111  psercnlem2  24223  psercnlem1  24224  psercn  24225  pserdvlem1  24226  pserdvlem2  24227  pserdv  24228  pserdv2  24229  abelthlem4  24233  abelthlem6  24235  abelthlem9  24239  abelth  24240  logcnlem5  24437  dvlog  24442  dvlog2lem  24443  dvlog2  24444  dvcncxp1  24529  dvcnsqrt  24530  cxpcn3lem  24533  cxpcn3  24534  sqrtcn  24536  1cubr  24614  atansssdm  24705  atancn  24708  jensen  24760  lgamucov  24809  lgamucov2  24810  ftalem3  24846  musum  24962  dvdsmulf1o  24965  fsumdvdsmul  24966  ppiub  24974  lgsfcl2  25073  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  2sqlem7  25194  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  dchrisum0  25254  pntlem3  25343  axtgcgrrflx  25406  axtgcgrid  25407  axtgsegcon  25408  axtg5seg  25409  axtgbtwnid  25410  axtgpasch  25411  axtgcont1  25412  tglng  25486  axcontlem2  25890  axcontlem7  25895  axcontlem8  25896  axcontlem10  25898  upgrreslem  26241  umgrreslem  26242  vtxdginducedm1lem2  26492  finsumvtxdg2ssteplem1  26497  disjxwwlkn  26876  clwwlknclwwlkdifnumOLD  26948  clwwlksswrd  26955  frgrwopreg2  27299  phnv  27797  htthlem  27902  hlimadd  28178  hlimcaui  28221  hhsscms  28264  occllem  28290  shjshsi  28479  3oalem4  28652  pjfi  28691  dmadjss  28874  nlelshi  29047  nlelchi  29048  hmopidmchi  29138  atssch  29330  shatomistici  29348  fcoinver  29544  opabssi  29551  mptctf  29623  fcobijfs  29629  psgnfzto1stlem  29978  cnre2csqima  30085  raddcn  30103  rrhre  30193  esumsnf  30254  sxbrsiga  30480  omssubadd  30490  carsggect  30508  sitmcl  30541  oddpwdc  30544  eulerpartlem1  30557  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemmf  30565  eulerpartlemgh  30568  sseqf  30582  ballotlemfmpn  30684  ballotth  30727  signswch  30766  ftc2re  30804  fdvposlt  30805  fdvposle  30807  bnj1146  30988  bnj1292  31012  bnj1293  31013  bnj1145  31187  bnj1177  31200  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem2  31300  kur14lem3  31316  kur14lem6  31319  kur14lem7  31320  kur14lem9  31322  cvmlift2lem12  31422  mpstssv  31562  mstapst  31570  mppspstlem  31594  mppspst  31597  mthmsta  31601  mthmpps  31605  mclsppslem  31606  dfpo2  31771  wlimss  31899  frrlem7  31915  nosupbnd1lem1  31979  nosupbnd2  31987  scutf  32044  txpss3v  32110  pprodss4v  32116  relsset  32120  fixssdm  32138  fixssrn  32139  limitssson  32143  funpartss  32176  colinearex  32292  fneer  32473  neibastop1  32479  neibastop2lem  32480  filnetlem2  32499  filnetlem3  32500  knoppcnlem10  32617  bj-tagss  33093  bj-cmnssmnd  33266  bj-ablssgrp  33268  bj-ablsscmn  33270  bj-vecssmod  33273  bj-rrvecssvec  33280  icoreresf  33330  icoreunrn  33337  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimir  33572  broucube  33573  dvasin  33626  dvacos  33627  areacirc  33635  caures  33686  bnd2lem  33720  ismtyres  33737  flddivrng  33928  xrnss3v  34274  toycom  34578  dihglblem2N  36900  lcdvbase  37199  mapdunirnN  37256  eldiophb  37637  monotuz  37823  fglmod  37960  pwssplit4  37976  pwfi2f1o  37983  arearect  38118  fvnonrel  38220  rclexi  38239  rtrclex  38241  trclexi  38244  rtrclexi  38245  clcnvlem  38247  cnvrcl0  38249  cnvtrcl0  38250  dfrtrcl5  38253  dfrcl2  38283  comptiunov2i  38315  corclrcl  38316  trclrelexplem  38320  relexpaddss  38327  cotrcltrcl  38334  corcltrcl  38348  cotrclrcl  38351  frege131d  38373  rp-imass  38382  0he  38393  uzmptshftfval  38862  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  rabexgf  39497  uzct  39546  disjf1o  39692  dmresss  39750  dmmptssf  39752  mptssid  39764  uzfissfz  39855  ssuzfz  39878  uzssre2  39946  uzublem  39970  uzssz2  39998  uzsscn2  40021  limcperiod  40178  sumnnodd  40180  climconstmpt  40208  fnlimfvre  40224  fnlimabslt  40229  limsupvaluz  40258  limsupubuzlem  40262  limsupubuz  40263  limsupequzmpt2  40268  limsupmnfuzlem  40276  limsupre3uzlem  40285  liminfequzmpt2  40341  cncfshift  40405  cncfperiod  40410  ibliooicc  40505  stoweidlem44  40579  stoweidlem50  40585  stoweidlem51  40586  stoweidlem52  40587  stoweidlem57  40592  stoweidlem59  40594  fourierdlem16  40658  fourierdlem19  40661  fourierdlem21  40663  fourierdlem22  40664  fourierdlem42  40684  fourierdlem83  40724  fouriersw  40766  salexct  40870  salexct3  40878  salgencntex  40879  salgensscntex  40880  sge0less  40927  sge0fodjrnlem  40951  sge0isum  40962  ovnsslelem  41095  ovnlerp  41097  ovn0lem  41100  hoidmv1lelem1  41126  hoidmv1lelem3  41128  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  ovnhoilem1  41136  ovnhoilem2  41137  opnvonmbllem2  41168  ovolval4lem1  41184  ovolval5lem3  41189  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  incsmflem  41271  decsmflem  41295  smflimlem2  41301  smflimlem3  41302  smflim  41306  smfrec  41317  smfmullem4  41322  smfdiv  41325  smfsuplem1  41338  smfsuplem3  41340  smfsupxr  41343  smfliminflem  41357  oddibas  42138  2zlidl  42259  2zrngbas  42261  2zrng0  42263  fldc  42408  fldhmsubc  42409  fldcALTV  42426  fldhmsubcALTV  42427  setrec2lem1  42765
  Copyright terms: Public domain W3C validator