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

Theorem eqsstri 3519
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1  |-  A  =  B
eqsstr.2  |-  B  C_  C
Assertion
Ref Expression
eqsstri  |-  A  C_  C

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2  |-  B  C_  C
2 eqsstr.1 . . 3  |-  A  =  B
32sseq1i 3513 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 209 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  eqsstr3i  3520  ssrab2  3571  rabssab  3573  opabss  4500  brab2ga  5064  relopabi  5116  dmopabss  5203  resss  5285  relres  5289  rnin  5400  rnxpss  5424  cnvcnvss  5445  dmmptss  5486  fnres  5679  f0  5748  nfvres  5878  fvopab4ndm  5954  ffvresb  6038  funiunfv  6135  isoini2  6210  ovssunirn  6299  dmoprabss  6357  mpt2ndm0  6489  elmpt2cl  6490  omsson  6677  exse2  6712  fabexg  6729  frxp  6883  tposssxp  6951  dftpos4  6966  smores  7015  smores2  7017  iordsmo  7020  oawordeulem  7195  swoer  7331  swoord1  7332  swoord2  7333  ecss  7345  ecopovsym  7405  ecopovtrn  7406  ecopover  7407  sbthlem7  7626  nnfi  7703  imafi  7805  elfiun  7882  marypha1lem  7885  marypha2lem1  7887  ordtypelem2  7936  hartogslem1  7959  wemapso2OLD  7969  wemapso2lem  7970  wdomima2g  8004  inf3lem1  8036  wemapwe  8130  wemapweOLD  8131  tc2  8164  tz9.12lem1  8196  rankuni  8272  rankuniss  8275  rankmapu  8287  cplem1  8298  hta  8306  r0weon  8381  infxpenlem  8382  ackbij1lem9  8599  ackbij1lem10  8600  ackbij1b  8610  cofsmo  8640  sdom2en01  8673  fin23lem26  8696  fin23lem28  8711  fin23lem30  8713  isf32lem5  8728  isf32lem6  8729  isf32lem7  8730  isf32lem8  8731  fin56  8764  fin1a2lem9  8779  hsmexlem4  8800  hsmexlem5  8801  hsmexlem6  8802  axdc3lem  8821  axdc3lem2  8822  axcclem  8828  zorn2lem1  8867  zorn2lem3  8869  zorn2lem4  8870  zorn2lem5  8871  imadomg  8903  iundom2g  8906  smobeth  8952  canth4  9014  gruina  9185  grur1a  9186  pinn  9245  niex  9248  ltsopi  9255  ltrelpi  9256  dmaddpi  9257  dmmulpi  9258  enqex  9289  0nnq  9291  elpqn  9292  ltrelnq  9293  nqerf  9297  nqerrel  9299  dmrecnq  9335  lterpq  9337  ltrelpr  9365  enrex  9433  ltrelsr  9434  dmaddsr  9451  dmmulsr  9452  ltrelre  9500  axaddf  9511  axmulf  9512  ltrelxr  9637  lerelxr  9639  nn0ssre  10795  nn0ssz  10881  uzsupss  11175  rpnnen1lem1  11209  rpnnen1lem2  11210  rpnnen1lem3  11211  rpnnen1lem5  11213  rpre  11227  uzsup  11972  fzfi  12067  swrd00  12637  sqrlem3  13163  sqrlem5  13165  cau3  13273  caubnd  13276  limsupgre  13389  rlimpm  13408  rlimclim  13454  isercolllem1  13572  isercolllem2  13573  isercoll  13575  caurcvg  13584  caucvg  13586  iseraltlem2  13590  iseraltlem3  13591  zsum  13625  fsumcvg3  13636  climfsum  13719  ackbijnn  13725  infcvgaux1i  13753  clim2prod  13782  ntrivcvg  13791  ntrivcvgfvn0  13793  ntrivcvgtail  13794  ntrivcvgmullem  13795  ntrivcvgmul  13796  zprod  13829  dvdszrcl  14078  divalglem2  14140  divalglem5  14142  divalglem8  14145  gcdcllem3  14238  bezoutlem2  14264  bezoutlem3  14265  maxprmfct  14341  phimullem  14396  eulerthlem2  14399  prmdiveq  14403  prmdivdiv  14404  pclem  14449  infpn2  14518  prmreclem2  14522  prmreclem3  14523  prmreclem5  14525  4sqlem1  14553  4sqlem13  14562  4sqlem14  14563  4sqlem17  14566  4sqlem18  14567  4sqlem19  14568  vdwnnlem3  14602  ramcl2lem  14614  ramtcl  14615  ramtcl2  14616  ramtub  14617  ramub1lem2  14632  structcnvcnv  14730  fvsetsid  14746  strlemor0  14813  strlemor1  14814  strleun  14817  imasdsval2  15008  gsumval1  16106  nmzsubg  16444  nmznsg  16447  conjnmz  16502  conjnmzb  16503  gicer  16526  gastacl  16549  symgbasfi  16613  mvdco  16672  symgsssg  16694  sylow1lem2  16821  sylow1lem3  16822  sylow1lem4  16823  sylow1lem5  16824  sylow2a  16841  sylow3lem2  16850  efglem  16936  efgtf  16942  efgtlen  16946  efginvrel2  16947  efginvrel1  16948  efgsfo  16959  efgredlemg  16962  efgredleme  16963  efgredlemd  16964  efgredlemc  16965  efgredlem  16967  efgred  16968  efgrelexlemb  16970  efgcpbllemb  16975  frgpinv  16984  frgpuplem  16992  frgpupf  16993  frgpup1  16995  frgpnabllem2  17080  gsumval3OLD  17110  gsumval3lem1  17111  gsumval3lem2  17112  gsumval3  17113  ablfacrplem  17314  ablfacrp2  17316  ablfac1eu  17322  pgpfaclem1  17330  ablfaclem2  17335  ablfaclem3  17336  lspsolvlem  17986  lbsextlem2  18003  lbsextlem3  18004  lbsextlem4  18005  rrgeq0  18136  rrgss  18139  psrbagconf1o  18224  psrass1lem  18227  mplbasss  18289  ply1bascl  18440  coe1mul2lem2  18507  znf1o  18766  zntoslem  18771  cygznlem2a  18782  psgnghm  18792  pjpm  18915  dsmmbase  18942  frlmsslsp  19001  mretopd  19763  ordtbas  19863  leordtval2  19883  lecldbas  19890  lmfval  19903  lmbrf  19931  cnconst2  19954  hauscmplem  20076  concompcld  20104  hauspwdom  20171  txuni2  20235  xkouni  20269  xkoccn  20289  txkgen  20322  qtoptop2  20369  kqdisj  20402  hmphtop  20448  hmpher  20454  uzrest  20567  uzfbas  20568  lmflf  20675  ptcmplem1  20721  ptcmplem3  20723  tgpconcompeqg  20779  tgpconcomp  20780  ustn0  20892  imasdsf1olem  21045  xmeter  21105  blcld  21177  isngp2  21286  xrtgioo  21480  iccntr  21495  icccmplem1  21496  icccmplem2  21497  icccmplem3  21498  xmetdcn  21512  metdcn  21514  metdscn2  21530  icchmeo  21610  cnheiborlem  21623  lmmbrf  21870  iscau4  21887  iscauf  21888  caucfil  21891  lmclimf  21911  rrxf  21997  ivthlem1  22032  ivthlem2  22033  ivthlem3  22034  ovolsslem  22064  ovolicc2lem3  22099  ovolicc2lem4  22100  ovolicc2lem5  22101  ovolicc2  22102  volf  22109  uniioombllem3  22163  uniioombllem4  22164  uniioombllem5  22165  dyadmbllem  22177  dyadmbl  22178  volcn  22184  mbfimaopnlem  22231  mbflimsup  22242  i1f1  22266  itg2lcl  22303  iblmbf  22343  itgioo  22391  itgsplitioo  22413  limcflflem  22453  limcflf  22454  limcresi  22458  lhop  22586  dvfsumlem1  22596  dvfsumlem2  22597  dvfsumlem3  22598  dvfsumlem4  22599  dvfsumrlimge0  22600  dvfsumrlim  22601  dvfsumrlim2  22602  dvfsum2  22604  vieta1lem1  22875  vieta1lem2  22876  psercnlem2  22988  psercnlem1  22989  psercn  22990  pserdvlem1  22991  pserdvlem2  22992  pserdv  22993  pserdv2  22994  abelthlem4  22998  abelthlem6  23000  abelthlem9  23004  abelth  23005  logcnlem5  23198  dvlog  23203  dvlog2lem  23204  dvlog2  23205  cxpcn3lem  23292  cxpcn3  23293  sqrtcn  23295  1cubr  23373  atansssdm  23464  atancn  23467  jensen  23519  wilthlem1  23543  ftalem3  23549  dvdsflip  23659  musum  23668  dvdsmulf1o  23671  fsumdvdsmul  23672  ppiub  23680  lgsfcl2  23778  lgsquadlem1  23830  lgsquadlem2  23831  lgsquadlem3  23832  2sqlem7  23846  rpvmasum2  23898  dchrisum0re  23899  dchrisum0lema  23900  dchrisum0lem1b  23901  dchrisum0lem1  23902  dchrisum0lem2a  23903  dchrisum0lem2  23904  dchrisum0lem3  23905  dchrisum0  23906  pntlem3  23995  axtgcgrrflx  24060  axtgcgrid  24061  axtgsegcon  24062  axtg5seg  24063  axtgbtwnid  24064  axtgpasch  24065  axtgcont1  24066  tglng  24137  axcontlem2  24473  axcontlem7  24478  axcontlem8  24479  axcontlem10  24481  nbgraf1olem1  24646  disjxwwlkn  24950  clwlknclwlkdifnum  25166  frgrawopreg1  25255  frgrawopreg2  25256  issubgoi  25513  flddivrng  25618  phnv  25930  htthlem  26035  hlimadd  26311  hlimcaui  26355  hhsscms  26396  occllem  26422  shjshsi  26611  3oalem4  26784  pjfi  26823  dmadjss  27007  nlelshi  27180  nlelchi  27181  hmopidmchi  27271  atssch  27463  shatomistici  27481  fcoinver  27677  mptexgf  27689  mptctf  27777  fcobijfs  27783  cnre2csqima  28131  raddcn  28149  rrhre  28236  esumsnf  28296  sxbrsiga  28501  omssubadd  28511  carsggect  28529  oddpwdc  28560  eulerpartlem1  28573  eulerpartlemt  28577  eulerpartgbij  28578  eulerpartlemmf  28581  eulerpartlemgvv  28582  eulerpartlemgh  28584  sseqf  28598  ballotlemfmpn  28700  ballotth  28743  signswch  28785  lgamucov  28847  lgamucov2  28848  subfacp1lem3  28893  subfacp1lem5  28895  erdszelem2  28903  kur14lem3  28919  kur14lem6  28922  kur14lem7  28923  kur14lem9  28925  cvmlift2lem12  29026  mpstssv  29166  mstapst  29174  mppspstlem  29198  mppspst  29201  mthmsta  29205  mthmpps  29209  mclsppslem  29210  ghomgrpilem2  29293  divcnvshft  29361  dfpo2  29428  predss  29494  wfrlem7  29592  wlimss  29628  frrlem7  29640  txpss3v  29759  pprodss4v  29765  relsset  29769  fixssdm  29787  fixssrn  29788  limitssson  29792  funpartss  29825  colinearex  29941  dvcncxp1  30343  dvcnsqrt  30344  dvasin  30346  dvacos  30347  areacirc  30355  fneer  30414  neibastop1  30420  neibastop2lem  30421  filnetlem2  30440  filnetlem3  30441  caures  30496  bnd2lem  30530  ismtyres  30547  eldiophb  30932  monotuz  31119  fglmod  31261  pwssplit4  31277  pwfi2f1o  31286  pwfi2f1oOLD  31287  arearect  31427  uzmptshftfval  31495  binomcxplemdvbinom  31502  binomcxplemdvsum  31504  binomcxplemnotnn0  31505  rabexgf  31642  fz1ssfz0  31752  limcperiod  31876  sumnnodd  31878  cncfshift  31918  cncfperiod  31923  ibliooicc  32012  stoweidlem26  32050  stoweidlem44  32068  stoweidlem50  32074  stoweidlem51  32075  stoweidlem52  32076  stoweidlem57  32081  stoweidlem59  32083  fourierdlem16  32147  fourierdlem19  32150  fourierdlem21  32152  fourierdlem22  32153  fourierdlem42  32173  fourierdlem83  32214  fouriersw  32256  oddibas  32892  2zlidl  33013  2zrngbas  33015  2zrng0  33017  fldc  33164  fldhmsubc  33165  fldcALTV  33183  fldhmsubcALTV  33184  bnj21  34190  bnj1146  34270  bnj1292  34294  bnj1293  34295  bnj1145  34469  bnj1177  34482  bj-tagss  34958  bj-cmnssmnd  35071  bj-ablssgrp  35073  bj-ablsscmn  35075  bj-vecssmod  35078  bj-rrvecssvec  35085  toycom  35114  dihglblem2N  37437  lcdvbase  37736  mapdunirnN  37793  dfrcl2  38214  relexpaddss  38226  comptiunov2i  38237  trclrelexplem  38250  corclrcl  38251  corcltrcl  38252  cotrclrcl  38253  cotrcltrcl  38254  rp-imass  38268  xphe  38278  0he  38279
  Copyright terms: Public domain W3C validator