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

Theorem eqsstri 3494
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 3488 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 212 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  eqsstr3i  3495  ssrab2  3546  rabssab  3548  opabss  4485  brab2ga  4929  relopabi  4978  dmopabss  5065  resss  5147  relres  5151  rnin  5264  rnxpss  5288  cnvcnvss  5309  dmmptss  5350  predss  5406  fnres  5710  f0  5781  nfvres  5911  fvopab4ndm  5988  ffvresb  6069  funiunfv  6168  isoini2  6245  ovssunirn  6334  dmoprabss  6392  mpt2ndm0  6524  elmpt2cl  6525  omsson  6710  exse2  6746  fabexg  6763  frxp  6917  tposssxp  6988  dftpos4  7003  wfrdmss  7053  smores  7082  smores2  7084  iordsmo  7087  oawordeulem  7266  swoer  7402  swoord1  7403  swoord2  7404  ecss  7416  ecopovsym  7476  ecopovtrn  7477  ecopover  7478  sbthlem7  7697  nnfi  7774  imafi  7876  elfiun  7953  marypha1lem  7956  marypha2lem1  7958  ordtypelem2  8043  hartogslem1  8066  wemapso2lem  8076  wdomima2g  8110  inf3lem1  8142  wemapwe  8210  tc2  8234  tz9.12lem1  8266  rankuni  8342  rankuniss  8345  rankmapu  8357  cplem1  8368  hta  8376  r0weon  8451  infxpenlem  8452  ackbij1lem9  8665  ackbij1lem10  8666  ackbij1b  8676  cofsmo  8706  sdom2en01  8739  fin23lem26  8762  fin23lem28  8777  fin23lem30  8779  isf32lem5  8794  isf32lem6  8795  isf32lem7  8796  isf32lem8  8797  fin56  8830  fin1a2lem9  8845  hsmexlem4  8866  hsmexlem5  8867  hsmexlem6  8868  axdc3lem  8887  axdc3lem2  8888  axcclem  8894  zorn2lem1  8933  zorn2lem3  8935  zorn2lem4  8936  zorn2lem5  8937  imadomg  8969  iundom2g  8972  smobeth  9018  canth4  9079  gruina  9250  grur1a  9251  pinn  9310  niex  9313  ltsopi  9320  ltrelpi  9321  dmaddpi  9322  dmmulpi  9323  enqex  9354  0nnq  9356  elpqn  9357  ltrelnq  9358  nqerf  9362  nqerrel  9364  dmrecnq  9400  lterpq  9402  ltrelpr  9430  enrex  9498  ltrelsr  9499  dmaddsr  9516  dmmulsr  9517  ltrelre  9565  axaddf  9576  axmulf  9577  ltrelxr  9702  lerelxr  9704  nn0ssre  10880  nn0ssz  10965  uzsupss  11263  rpnnen1lem1  11297  rpnnen1lem2  11298  rpnnen1lem3  11299  rpnnen1lem5  11301  rpre  11315  uzsup  12096  fzfi  12191  swrd00  12776  sqrlem3  13308  sqrlem5  13310  cau3  13418  caubnd  13421  limsupgre  13541  limsupgreOLD  13542  rlimpm  13563  rlimclim  13609  isercolllem1  13727  isercolllem2  13728  isercoll  13730  caurcvg  13741  caurcvgOLD  13742  caucvg  13744  iseraltlem2  13748  iseraltlem3  13749  zsum  13783  fsumcvg3  13794  climfsum  13879  ackbijnn  13885  divcnvshft  13912  infcvgaux1i  13914  clim2prod  13943  ntrivcvg  13952  ntrivcvgfvn0  13954  ntrivcvgtail  13955  ntrivcvgmullem  13956  ntrivcvgmul  13957  zprod  13990  dvdszrcl  14309  divalglem2  14372  divalglem2OLD  14373  divalglem5OLD  14375  divalglem5  14376  divalglem8  14379  gcdcllem3  14474  bezoutlem2OLD  14503  bezoutlem3OLD  14504  bezoutlem2  14506  bezoutlem3  14507  maxprmfct  14651  phimullem  14726  eulerthlem2  14729  prmdiveq  14733  prmdivdiv  14734  pclem  14787  infpn2  14856  prmreclem2  14860  prmreclem3  14861  prmreclem5  14863  4sqlem1  14891  4sqlem13OLD  14900  4sqlem14OLD  14901  4sqlem17OLD  14904  4sqlem18OLD  14905  4sqlem13  14906  4sqlem14  14907  4sqlem17  14910  4sqlem18  14911  4sqlem19  14912  vdwnnlem3  14946  ramcl2lem  14961  ramcl2lemOLD  14962  ramtcl  14963  ramtclOLD  14964  ramtcl2  14965  ramtcl2OLD  14966  ramtub  14967  ramtubOLD  14968  ramub1lem2  14984  structcnvcnv  15131  fvsetsid  15147  strlemor0  15215  strlemor1  15216  strleun  15219  imasdsval2  15416  imasdsval2OLD  15428  gsumval1  16519  nmzsubg  16857  nmznsg  16860  conjnmz  16915  conjnmzb  16916  gicer  16939  gastacl  16962  symgbasfi  17026  mvdco  17085  symgsssg  17107  sylow1lem2  17250  sylow1lem3  17251  sylow1lem4  17252  sylow1lem5  17253  sylow2a  17270  sylow3lem2  17279  efglem  17365  efgtf  17371  efgtlen  17375  efginvrel2  17376  efginvrel1  17377  efgsfo  17388  efgredlemg  17391  efgredleme  17392  efgredlemd  17393  efgredlemc  17394  efgredlem  17396  efgred  17397  efgrelexlemb  17399  efgcpbllemb  17404  frgpinv  17413  frgpuplem  17421  frgpupf  17422  frgpup1  17424  frgpnabllem2  17509  gsumval3lem1  17538  gsumval3lem2  17539  gsumval3  17540  ablfacrplem  17697  ablfacrp2  17699  ablfac1eu  17705  pgpfaclem1  17713  ablfaclem2  17718  ablfaclem3  17719  lspsolvlem  18364  lbsextlem2  18381  lbsextlem3  18382  lbsextlem4  18383  rrgeq0  18513  rrgss  18515  psrbagconf1o  18597  psrass1lem  18600  mplbasss  18655  ply1bascl  18795  coe1mul2lem2  18860  znf1o  19120  zntoslem  19125  cygznlem2a  19136  psgnghm  19146  pjpm  19269  dsmmbase  19296  frlmsslsp  19352  mretopd  20106  ordtbas  20206  leordtval2  20226  lecldbas  20233  lmfval  20246  lmbrf  20274  cnconst2  20297  hauscmplem  20419  concompcld  20447  hauspwdom  20514  txuni2  20578  xkouni  20612  xkoccn  20632  txkgen  20665  qtoptop2  20712  kqdisj  20745  hmphtop  20791  hmpher  20797  uzrest  20910  uzfbas  20911  lmflf  21018  ptcmplem1  21065  ptcmplem3  21067  tgpconcompeqg  21124  tgpconcomp  21125  ustn0  21233  imasdsf1olem  21386  xmeter  21446  blcld  21518  isngp2  21609  xrtgioo  21822  iccntr  21837  icccmplem1  21838  icccmplem2  21839  icccmplem3  21840  xmetdcn  21854  metdcn  21856  metdscn2  21872  metdscn2OLD  21887  icchmeo  21967  cnheiborlem  21980  lmmbrf  22230  iscau4  22247  iscauf  22248  caucfil  22251  lmclimf  22271  rrxf  22353  ivthlem1  22400  ivthlem2  22401  ivthlem3  22402  ovolsslem  22435  ovolicc2lem3  22470  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  ovolicc2  22474  volf  22481  uniioombllem3  22541  uniioombllem4  22542  uniioombllem5  22543  dyadmbllem  22555  dyadmbl  22556  volcn  22562  mbfimaopnlem  22609  mbflimsup  22621  mbflimsupOLD  22622  i1f1  22646  itg2lcl  22683  iblmbf  22723  itgioo  22771  itgsplitioo  22793  limcflflem  22833  limcflf  22834  limcresi  22838  lhop  22966  dvfsumlem1  22976  dvfsumlem2  22977  dvfsumlem3  22978  dvfsumlem4  22979  dvfsumrlimge0  22980  dvfsumrlim  22981  dvfsumrlim2  22982  dvfsum2  22984  vieta1lem1  23261  vieta1lem2  23262  psercnlem2  23377  psercnlem1  23378  psercn  23379  pserdvlem1  23380  pserdvlem2  23381  pserdv  23382  pserdv2  23383  abelthlem4  23387  abelthlem6  23389  abelthlem9  23393  abelth  23394  logcnlem5  23589  dvlog  23594  dvlog2lem  23595  dvlog2  23596  dvcncxp1  23681  dvcnsqrt  23682  cxpcn3lem  23685  cxpcn3  23686  sqrtcn  23688  1cubr  23766  atansssdm  23857  atancn  23860  jensen  23912  lgamucov  23961  lgamucov2  23962  wilthlem1  23991  ftalem3  23997  dvdsflip  24109  musum  24118  dvdsmulf1o  24121  fsumdvdsmul  24122  ppiub  24130  lgsfcl2  24228  lgsquadlem1  24280  lgsquadlem2  24281  lgsquadlem3  24282  2sqlem7  24296  rpvmasum2  24348  dchrisum0re  24349  dchrisum0lema  24350  dchrisum0lem1b  24351  dchrisum0lem1  24352  dchrisum0lem2a  24353  dchrisum0lem2  24354  dchrisum0lem3  24355  dchrisum0  24356  pntlem3  24445  axtgcgrrflx  24508  axtgcgrid  24509  axtgsegcon  24510  axtg5seg  24511  axtgbtwnid  24512  axtgpasch  24513  axtgcont1  24514  tglng  24589  axcontlem2  24993  axcontlem7  24998  axcontlem8  24999  axcontlem10  25001  nbgraf1olem1  25167  disjxwwlkn  25471  clwlknclwlkdifnum  25687  frgrawopreg1  25776  frgrawopreg2  25777  issubgoi  26036  flddivrng  26141  phnv  26453  htthlem  26568  hlimadd  26844  hlimcaui  26887  hhsscms  26928  occllem  26954  shjshsi  27143  3oalem4  27316  pjfi  27355  dmadjss  27538  nlelshi  27711  nlelchi  27712  hmopidmchi  27802  atssch  27994  shatomistici  28012  fcoinver  28216  mptexgf  28227  mptctf  28311  fcobijfs  28317  psgnfzto1stlem  28621  cnre2csqima  28725  raddcn  28743  rrhre  28833  esumsnf  28893  sxbrsiga  29120  omssubadd  29136  omssubaddOLD  29140  carsggect  29158  sitmcl  29192  oddpwdc  29195  eulerpartlem1  29208  eulerpartlemt  29212  eulerpartgbij  29213  eulerpartlemmf  29216  eulerpartlemgvv  29217  eulerpartlemgh  29219  sseqf  29233  ballotlemfmpn  29335  ballotth  29378  ballotthOLD  29416  signswch  29458  bnj21  29531  bnj1146  29611  bnj1292  29635  bnj1293  29636  bnj1145  29810  bnj1177  29823  subfacp1lem3  29913  subfacp1lem5  29915  erdszelem2  29923  kur14lem3  29939  kur14lem6  29942  kur14lem7  29943  kur14lem9  29945  cvmlift2lem12  30045  mpstssv  30185  mstapst  30193  mppspstlem  30217  mppspst  30220  mthmsta  30224  mthmpps  30228  mclsppslem  30229  ghomgrpilem2  30312  dfpo2  30402  wlimss  30519  frrlem7  30531  txpss3v  30650  pprodss4v  30656  relsset  30660  fixssdm  30678  fixssrn  30679  limitssson  30683  funpartss  30716  colinearex  30832  fneer  31014  neibastop1  31020  neibastop2lem  31021  filnetlem2  31040  filnetlem3  31041  bj-tagss  31542  bj-cmnssmnd  31655  bj-ablssgrp  31657  bj-ablsscmn  31659  bj-vecssmod  31662  bj-rrvecssvec  31669  icoreresf  31719  icoreunrn  31726  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  poimir  31937  broucube  31938  dvasin  31992  dvacos  31993  areacirc  32001  caures  32053  bnd2lem  32087  ismtyres  32104  toycom  32508  dihglblem2N  34831  lcdvbase  35130  mapdunirnN  35187  eldiophb  35568  monotuz  35759  fglmod  35901  pwssplit4  35917  pwfi2f1o  35924  arearect  36070  fvnonrel  36173  rclexi  36192  rtrclex  36194  trclexi  36197  rtrclexi  36198  clcnvlem  36200  cnvrcl0  36202  cnvtrcl0  36203  dfrtrcl5  36206  dfrcl2  36236  comptiunov2i  36268  corclrcl  36269  trclrelexplem  36273  relexpaddss  36280  cotrcltrcl  36287  corcltrcl  36301  cotrclrcl  36304  frege131d  36326  rp-imass  36336  xpheOLD  36347  0he  36348  uzmptshftfval  36665  binomcxplemdvbinom  36672  binomcxplemdvsum  36674  binomcxplemnotnn0  36675  rabexgf  37318  uzct  37377  disjf1o  37427  fz1ssfz0  37482  uzfissfz  37503  ssuzfz  37526  limcperiod  37648  sumnnodd  37650  cncfshift  37691  cncfperiod  37696  ibliooicc  37788  stoweidlem26  37826  stoweidlem44  37845  stoweidlem50  37851  stoweidlem51  37852  stoweidlem52  37853  stoweidlem57  37858  stoweidlem59  37860  fourierdlem16  37925  fourierdlem19  37928  fourierdlem21  37930  fourierdlem22  37931  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem83  37993  fouriersw  38035  sge0less  38142  sge0fodjrnlem  38166  sge0isum  38177  ovnsslelem  38286  ovnlerp  38288  ovn0lem  38291  hoidmv1lelem1  38317  hoidmv1lelem3  38319  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  hoidmvlelem4  38324  ovnhoilem1  38327  ovnhoilem2  38328  oddibas  39433  2zlidl  39554  2zrngbas  39556  2zrng0  39558  fldc  39705  fldhmsubc  39706  fldcALTV  39724  fldhmsubcALTV  39725
  Copyright terms: Public domain W3C validator