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

Theorem eqsstri 3430
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 3424 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 214 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1448    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386
This theorem is referenced by:  eqsstr3i  3431  ssrab2  3482  rabssab  3484  opabss  4436  brab2ga  4888  relopabi  4937  dmopabss  5024  resss  5106  relres  5110  rnin  5223  rnxpss  5247  cnvcnvss  5269  dmmptss  5310  predss  5366  fnres  5674  f0  5747  nfvres  5878  fvopab4ndm  5956  ffvresb  6039  funiunfv  6139  isoini2  6216  ovssunirn  6305  dmoprabss  6366  mpt2ndm0  6498  elmpt2cl  6499  omsson  6684  exse2  6720  fabexg  6737  frxp  6894  tposssxp  6964  dftpos4  6979  wfrdmss  7029  smores  7058  smores2  7060  iordsmo  7063  oawordeulem  7242  swoer  7378  swoord1  7379  swoord2  7380  ecss  7392  ecopovsym  7452  ecopovtrn  7453  ecopover  7454  sbthlem7  7675  nnfi  7752  imafi  7854  elfiun  7931  marypha1lem  7934  marypha2lem1  7936  ordtypelem2  8021  hartogslem1  8044  wemapso2lem  8054  wdomima2g  8088  inf3lem1  8120  wemapwe  8189  tc2  8213  tz9.12lem1  8245  rankuni  8321  rankuniss  8324  rankmapu  8336  cplem1  8347  hta  8355  r0weon  8430  infxpenlem  8431  ackbij1lem9  8645  ackbij1lem10  8646  ackbij1b  8656  cofsmo  8686  sdom2en01  8719  fin23lem26  8742  fin23lem28  8757  fin23lem30  8759  isf32lem5  8774  isf32lem6  8775  isf32lem7  8776  isf32lem8  8777  fin56  8810  fin1a2lem9  8825  hsmexlem4  8846  hsmexlem5  8847  hsmexlem6  8848  axdc3lem  8867  axdc3lem2  8868  axcclem  8874  zorn2lem1  8913  zorn2lem3  8915  zorn2lem4  8916  zorn2lem5  8917  imadomg  8949  iundom2g  8952  smobeth  8998  canth4  9059  gruina  9230  grur1a  9231  pinn  9290  niex  9293  ltsopi  9300  ltrelpi  9301  dmaddpi  9302  dmmulpi  9303  enqex  9334  0nnq  9336  elpqn  9337  ltrelnq  9338  nqerf  9342  nqerrel  9344  dmrecnq  9380  lterpq  9382  ltrelpr  9410  enrex  9478  ltrelsr  9479  dmaddsr  9496  dmmulsr  9497  ltrelre  9545  axaddf  9556  axmulf  9557  ltrelxr  9682  lerelxr  9684  nn0ssre  10863  nn0ssz  10948  uzsupss  11246  rpnnen1lem1  11280  rpnnen1lem2  11281  rpnnen1lem3  11282  rpnnen1lem5  11284  rpre  11298  uzsup  12084  fzfi  12179  swrd00  12773  sqrlem3  13319  sqrlem5  13321  cau3  13429  caubnd  13432  limsupgre  13553  limsupgreOLD  13554  rlimpm  13575  rlimclim  13621  isercolllem1  13739  isercolllem2  13740  isercoll  13742  caurcvg  13753  caurcvgOLD  13754  caucvg  13756  iseraltlem2  13760  iseraltlem3  13761  zsum  13795  fsumcvg3  13806  climfsum  13891  ackbijnn  13897  divcnvshft  13924  infcvgaux1i  13926  clim2prod  13955  ntrivcvg  13964  ntrivcvgfvn0  13966  ntrivcvgtail  13967  ntrivcvgmullem  13968  ntrivcvgmul  13969  zprod  14002  dvdszrcl  14321  divalglem2  14384  divalglem2OLD  14385  divalglem5OLD  14387  divalglem5  14388  divalglem8  14391  gcdcllem3  14486  bezoutlem2OLD  14515  bezoutlem3OLD  14516  bezoutlem2  14518  bezoutlem3  14519  maxprmfct  14663  phimullem  14738  eulerthlem2  14741  prmdiveq  14745  prmdivdiv  14746  pclem  14799  infpn2  14868  prmreclem2  14872  prmreclem3  14873  prmreclem5  14875  4sqlem1  14903  4sqlem13OLD  14912  4sqlem14OLD  14913  4sqlem17OLD  14916  4sqlem18OLD  14917  4sqlem13  14918  4sqlem14  14919  4sqlem17  14922  4sqlem18  14923  4sqlem19  14924  vdwnnlem3  14958  ramcl2lem  14973  ramcl2lemOLD  14974  ramtcl  14975  ramtclOLD  14976  ramtcl2  14977  ramtcl2OLD  14978  ramtub  14979  ramtubOLD  14980  ramub1lem2  14996  structcnvcnv  15143  fvsetsid  15159  strlemor0  15227  strlemor1  15228  strleun  15231  imasdsval2  15428  imasdsval2OLD  15440  gsumval1  16531  nmzsubg  16869  nmznsg  16872  conjnmz  16927  conjnmzb  16928  gicer  16951  gastacl  16974  symgbasfi  17038  mvdco  17097  symgsssg  17119  sylow1lem2  17262  sylow1lem3  17263  sylow1lem4  17264  sylow1lem5  17265  sylow2a  17282  sylow3lem2  17291  efglem  17377  efgtf  17383  efgtlen  17387  efginvrel2  17388  efginvrel1  17389  efgsfo  17400  efgredlemg  17403  efgredleme  17404  efgredlemd  17405  efgredlemc  17406  efgredlem  17408  efgred  17409  efgrelexlemb  17411  efgcpbllemb  17416  frgpinv  17425  frgpuplem  17433  frgpupf  17434  frgpup1  17436  frgpnabllem2  17521  gsumval3lem1  17550  gsumval3lem2  17551  gsumval3  17552  ablfacrplem  17709  ablfacrp2  17711  ablfac1eu  17717  pgpfaclem1  17725  ablfaclem2  17730  ablfaclem3  17731  lspsolvlem  18376  lbsextlem2  18393  lbsextlem3  18394  lbsextlem4  18395  rrgeq0  18525  rrgss  18527  psrbagconf1o  18609  psrass1lem  18612  mplbasss  18667  ply1bascl  18807  coe1mul2lem2  18872  znf1o  19133  zntoslem  19138  cygznlem2a  19149  psgnghm  19159  pjpm  19282  dsmmbase  19309  frlmsslsp  19365  mretopd  20119  ordtbas  20219  leordtval2  20239  lecldbas  20246  lmfval  20259  lmbrf  20287  cnconst2  20310  hauscmplem  20432  concompcld  20460  hauspwdom  20527  txuni2  20591  xkouni  20625  xkoccn  20645  txkgen  20678  qtoptop2  20725  kqdisj  20758  hmphtop  20804  hmpher  20810  uzrest  20923  uzfbas  20924  lmflf  21031  ptcmplem1  21078  ptcmplem3  21080  tgpconcompeqg  21137  tgpconcomp  21138  ustn0  21246  imasdsf1olem  21399  xmeter  21459  blcld  21531  isngp2  21622  xrtgioo  21835  iccntr  21850  icccmplem1  21851  icccmplem2  21852  icccmplem3  21853  xmetdcn  21867  metdcn  21869  metdscn2  21885  metdscn2OLD  21900  icchmeo  21980  cnheiborlem  21993  lmmbrf  22243  iscau4  22260  iscauf  22261  caucfil  22264  lmclimf  22284  rrxf  22366  ivthlem1  22413  ivthlem2  22414  ivthlem3  22415  ovolsslem  22448  ovolicc2lem3  22483  ovolicc2lem4OLD  22484  ovolicc2lem4  22485  ovolicc2lem5  22486  ovolicc2  22487  volf  22494  uniioombllem3  22555  uniioombllem4  22556  uniioombllem5  22557  dyadmbllem  22569  dyadmbl  22570  volcn  22576  mbfimaopnlem  22623  mbflimsup  22635  mbflimsupOLD  22636  i1f1  22660  itg2lcl  22697  iblmbf  22737  itgioo  22785  itgsplitioo  22807  limcflflem  22847  limcflf  22848  limcresi  22852  lhop  22980  dvfsumlem1  22990  dvfsumlem2  22991  dvfsumlem3  22992  dvfsumlem4  22993  dvfsumrlimge0  22994  dvfsumrlim  22995  dvfsumrlim2  22996  dvfsum2  22998  vieta1lem1  23275  vieta1lem2  23276  psercnlem2  23391  psercnlem1  23392  psercn  23393  pserdvlem1  23394  pserdvlem2  23395  pserdv  23396  pserdv2  23397  abelthlem4  23401  abelthlem6  23403  abelthlem9  23407  abelth  23408  logcnlem5  23603  dvlog  23608  dvlog2lem  23609  dvlog2  23610  dvcncxp1  23695  dvcnsqrt  23696  cxpcn3lem  23699  cxpcn3  23700  sqrtcn  23702  1cubr  23780  atansssdm  23871  atancn  23874  jensen  23926  lgamucov  23975  lgamucov2  23976  wilthlem1  24005  ftalem3  24011  dvdsflip  24123  musum  24132  dvdsmulf1o  24135  fsumdvdsmul  24136  ppiub  24144  lgsfcl2  24242  lgsquadlem1  24294  lgsquadlem2  24295  lgsquadlem3  24296  2sqlem7  24310  rpvmasum2  24362  dchrisum0re  24363  dchrisum0lema  24364  dchrisum0lem1b  24365  dchrisum0lem1  24366  dchrisum0lem2a  24367  dchrisum0lem2  24368  dchrisum0lem3  24369  dchrisum0  24370  pntlem3  24459  axtgcgrrflx  24522  axtgcgrid  24523  axtgsegcon  24524  axtg5seg  24525  axtgbtwnid  24526  axtgpasch  24527  axtgcont1  24528  tglng  24603  axcontlem2  25007  axcontlem7  25012  axcontlem8  25013  axcontlem10  25015  nbgraf1olem1  25181  disjxwwlkn  25485  clwlknclwlkdifnum  25701  frgrawopreg1  25790  frgrawopreg2  25791  issubgoi  26050  flddivrng  26155  phnv  26467  htthlem  26582  hlimadd  26858  hlimcaui  26901  hhsscms  26942  occllem  26968  shjshsi  27157  3oalem4  27330  pjfi  27369  dmadjss  27552  nlelshi  27725  nlelchi  27726  hmopidmchi  27816  atssch  28008  shatomistici  28026  fcoinver  28223  mptexgf  28234  mptctf  28313  fcobijfs  28319  psgnfzto1stlem  28620  cnre2csqima  28724  raddcn  28742  rrhre  28832  esumsnf  28892  sxbrsiga  29118  omssubadd  29134  omssubaddOLD  29138  carsggect  29156  sitmcl  29190  oddpwdc  29193  eulerpartlem1  29206  eulerpartlemt  29210  eulerpartgbij  29211  eulerpartlemmf  29214  eulerpartlemgvv  29215  eulerpartlemgh  29217  sseqf  29231  ballotlemfmpn  29333  ballotth  29376  ballotthOLD  29414  signswch  29456  bnj21  29529  bnj1146  29609  bnj1292  29633  bnj1293  29634  bnj1145  29808  bnj1177  29821  subfacp1lem3  29911  subfacp1lem5  29913  erdszelem2  29921  kur14lem3  29937  kur14lem6  29940  kur14lem7  29941  kur14lem9  29943  cvmlift2lem12  30043  mpstssv  30183  mstapst  30191  mppspstlem  30215  mppspst  30218  mthmsta  30222  mthmpps  30226  mclsppslem  30227  ghomgrpilem2  30310  dfpo2  30401  wlimss  30518  frrlem7  30530  txpss3v  30651  pprodss4v  30657  relsset  30661  fixssdm  30679  fixssrn  30680  limitssson  30684  funpartss  30717  colinearex  30833  fneer  31015  neibastop1  31021  neibastop2lem  31022  filnetlem2  31041  filnetlem3  31042  bj-tagss  31576  bj-cmnssmnd  31693  bj-ablssgrp  31695  bj-ablsscmn  31697  bj-vecssmod  31700  bj-rrvecssvec  31707  icoreresf  31757  icoreunrn  31764  poimirlem29  31971  poimirlem30  31972  poimirlem31  31973  poimir  31975  broucube  31976  dvasin  32030  dvacos  32031  areacirc  32039  caures  32091  bnd2lem  32125  ismtyres  32142  toycom  32541  dihglblem2N  34864  lcdvbase  35163  mapdunirnN  35220  eldiophb  35601  monotuz  35791  fglmod  35933  pwssplit4  35949  pwfi2f1o  35956  arearect  36102  fvnonrel  36205  rclexi  36224  rtrclex  36226  trclexi  36229  rtrclexi  36230  clcnvlem  36232  cnvrcl0  36234  cnvtrcl0  36235  dfrtrcl5  36238  dfrcl2  36268  comptiunov2i  36300  corclrcl  36301  trclrelexplem  36305  relexpaddss  36312  cotrcltrcl  36319  corcltrcl  36333  cotrclrcl  36336  frege131d  36358  rp-imass  36368  xpheOLD  36379  0he  36380  uzmptshftfval  36696  binomcxplemdvbinom  36703  binomcxplemdvsum  36705  binomcxplemnotnn0  36706  rabexgf  37342  uzct  37399  disjf1o  37476  fz1ssfz0  37559  uzfissfz  37580  ssuzfz  37603  limcperiod  37750  sumnnodd  37752  cncfshift  37793  cncfperiod  37798  ibliooicc  37890  stoweidlem26  37943  stoweidlem44  37962  stoweidlem50  37968  stoweidlem51  37969  stoweidlem52  37970  stoweidlem57  37975  stoweidlem59  37977  fourierdlem16  38042  fourierdlem19  38045  fourierdlem21  38047  fourierdlem22  38048  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem83  38110  fouriersw  38152  salexct  38250  salexct3  38258  salgencntex  38259  salgensscntex  38260  sge0less  38293  sge0fodjrnlem  38317  sge0isum  38328  ovnsslelem  38445  ovnlerp  38447  ovn0lem  38450  hoidmv1lelem1  38476  hoidmv1lelem3  38478  hoidmvlelem1  38480  hoidmvlelem2  38481  hoidmvlelem3  38482  hoidmvlelem4  38483  ovnhoilem1  38486  ovnhoilem2  38487  opnvonmbllem2  38518  ovolval4lem1  38534  ovolval5lem3  38539  oddibas  40138  2zlidl  40259  2zrngbas  40261  2zrng0  40263  fldc  40410  fldhmsubc  40411  fldcALTV  40429  fldhmsubcALTV  40430
  Copyright terms: Public domain W3C validator