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

Theorem eqsstri 3208
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 3202 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 200 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3152
This theorem is referenced by:  eqsstr3i  3209  ssrab2  3258  rabssab  3259  opabss  4080  epse  4376  omsson  4660  brab2ga  4763  relopabi  4811  dmopabss  4890  resss  4979  relres  4983  exse2  5047  rnin  5090  rnxpss  5108  cnvcnvss  5128  dmmptss  5169  fnres  5360  fabexg  5422  f0  5425  nfvres  5557  fvopab4ndm  5620  ffvresb  5690  funiunfv  5774  isoini2  5836  ovssunirn  5884  dmoprabss  5929  elmpt2cl  6061  frxp  6225  tposssxp  6238  dftpos4  6253  smores  6369  smores2  6371  iordsmo  6374  oawordeulem  6552  swoer  6688  swoord1  6689  swoord2  6690  ecss  6701  ecopovsym  6760  ecopovtrn  6761  ecopover  6762  sbthlem7  6977  nnfi  7053  imafi  7148  elfiun  7183  marypha1lem  7186  marypha2lem1  7188  ordtypelem2  7234  hartogslem1  7257  wemapso2  7267  wdomima2g  7300  inf3lem1  7329  cantnfres  7379  wemapwe  7400  tc2  7427  tz9.12lem1  7459  rankuni  7535  rankuniss  7538  cplem1  7559  hta  7567  r0weon  7640  infxpenlem  7641  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1b  7865  cofsmo  7895  sdom2en01  7928  fin23lem26  7951  fin23lem28  7966  fin23lem30  7968  isf32lem5  7983  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  fin56  8019  fin1a2lem9  8034  hsmexlem4  8055  hsmexlem5  8056  hsmexlem6  8057  axdc3lem  8076  axdc3lem2  8077  axcclem  8083  zorn2lem1  8123  zorn2lem3  8125  zorn2lem4  8126  zorn2lem5  8127  imadomg  8159  iundom2g  8162  smobeth  8208  canth4  8269  gruina  8440  grur1a  8441  pinn  8502  niex  8505  ltsopi  8512  ltrelpi  8513  dmaddpi  8514  dmmulpi  8515  enqex  8546  0nnq  8548  elpqn  8549  ltrelnq  8550  nqerf  8554  nqerrel  8556  dmrecnq  8592  lterpq  8594  ltrelpr  8622  enrex  8692  ltrelsr  8693  dmaddsr  8707  dmmulsr  8708  ltrelre  8756  axaddf  8767  axmulf  8768  ltrelxr  8886  lerelxr  8888  nn0ssre  9969  nn0ssz  10044  uzsupss  10310  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  rpre  10360  uzsup  10967  fzfi  11034  swrd00  11451  sqrlem3  11730  sqrlem5  11732  cau3  11839  caubnd  11842  limsupgre  11955  rlimpm  11974  rlimclim  12020  isercolllem1  12138  isercolllem2  12139  isercoll  12141  caurcvg  12149  caucvg  12151  iseraltlem2  12155  iseraltlem3  12156  zsum  12191  fsumcvg3  12202  climfsum  12278  ackbijnn  12286  infcvgaux1i  12315  dvdszrcl  12536  divalglem2  12594  divalglem5  12596  divalglem8  12599  gcdcllem3  12692  bezoutlem2  12718  bezoutlem3  12719  maxprmfct  12792  phimullem  12847  eulerthlem2  12850  prmdiveq  12854  prmdivdiv  12855  pclem  12891  infpn2  12960  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  4sqlem1  12995  4sqlem13  13004  4sqlem14  13005  4sqlem17  13008  4sqlem18  13009  4sqlem19  13010  vdwnnlem3  13044  ramcl2lem  13056  ramtcl  13057  ramtcl2  13058  ramtub  13059  ramub1lem2  13074  structcnvcnv  13159  strlemor0  13234  strlemor1  13235  strleun  13238  prdsval  13355  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdshom  13366  imasdsval2  13419  gsumval1  14456  nmzsubg  14658  nmznsg  14661  conjnmz  14716  conjnmzb  14717  gicer  14740  gastacl  14763  sylow1lem2  14910  sylow1lem3  14911  sylow1lem4  14912  sylow1lem5  14913  sylow2a  14930  sylow3lem2  14939  efglem  15025  efgtf  15031  efgtlen  15035  efginvrel2  15036  efginvrel1  15037  efgsfo  15048  efgredlemg  15051  efgredleme  15052  efgredlemd  15053  efgredlemc  15054  efgredlem  15056  efgred  15057  efgrelexlemb  15059  efgcpbllemb  15064  frgpinv  15073  frgpuplem  15081  frgpupf  15082  frgpup1  15084  frgpnabllem2  15162  gsumval3  15191  ablfacrplem  15300  ablfacrp2  15302  ablfac1eu  15308  pgpfaclem1  15316  ablfaclem2  15321  ablfaclem3  15322  lspsolvlem  15895  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  rrgeq0  16031  rrgss  16033  psrbagconf1o  16120  psrass1lem  16123  mplbasss  16177  ply1bascl  16284  coe1mul2lem2  16345  znf1o  16505  zntoslem  16510  cygznlem2a  16521  pjpm  16608  mretopd  16829  ordtbas  16922  leordtval2  16942  lecldbas  16949  lmfval  16962  lmbrf  16990  cnconst2  17011  hauscmplem  17133  concompcld  17160  hauspwdom  17227  txuni2  17260  xkouni  17294  xkoccn  17313  txkgen  17346  qtoptop2  17390  kqdisj  17423  hmphtop  17469  hmpher  17475  uzrest  17592  uzfbas  17593  lmflf  17700  ptcmplem1  17746  ptcmplem3  17748  tgpconcompeqg  17794  tgpconcomp  17795  imasdsf1olem  17937  xmeter  17979  blcld  18051  isngp2  18119  xrtgioo  18312  iccntr  18326  icccmplem1  18327  icccmplem2  18328  icccmplem3  18329  xmetdcn  18343  metdcn  18345  metdscn2  18361  icchmeo  18439  cnheiborlem  18452  lmmbrf  18688  iscau4  18705  iscauf  18706  caucfil  18709  lmclimf  18729  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  ovolsslem  18843  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  ovolicc2  18881  volf  18888  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  dyadmbllem  18954  dyadmbl  18955  volcn  18961  mbfimaopnlem  19010  mbflimsup  19021  i1f1  19045  itg2lcl  19082  iblmbf  19122  itgioo  19170  itgsplitioo  19192  limcflflem  19230  limcflf  19231  limcresi  19235  lhop  19363  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlimge0  19377  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsum2  19381  vieta1lem1  19690  vieta1lem2  19691  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  pserdv  19805  pserdv2  19806  abelthlem4  19810  abelthlem6  19812  abelthlem9  19816  abelth  19817  logcnlem5  19993  dvlog  19998  dvlog2lem  19999  dvlog2  20000  cxpcn3lem  20087  cxpcn3  20088  sqrcn  20090  1cubr  20138  atansssdm  20229  atancn  20232  jensen  20283  wilthlem1  20306  ftalem3  20312  dvdsflip  20422  musum  20431  dvdsmulf1o  20434  fsumdvdsmul  20435  ppiub  20443  lgsfcl2  20541  lgseisenlem3  20590  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  2sqlem7  20609  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  dchrisum0  20669  pntlem3  20758  issubgoi  20977  flddivrng  21082  phnv  21392  htthlem  21497  hlimadd  21772  hlimcaui  21816  hhsscms  21856  occllem  21882  shjshsi  22071  3oalem4  22244  pjfi  22283  dmadjss  22467  nlelshi  22640  nlelchi  22641  hmopidmchi  22731  atssch  22923  shatomistici  22941  ballotlemoex  23044  ballotlemfmpn  23053  ballotth  23096  cnre2csqima  23295  raddcn  23302  mptctf  23348  esumsn  23437  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem2  23723  kur14lem3  23739  kur14lem6  23742  kur14lem7  23743  kur14lem9  23745  cvmlift2lem12  23845  ghomgrpilem2  23993  dfpo2  24112  predss  24173  wfrlem7  24262  frrlem7  24291  txpss3v  24418  pprodss4v  24424  relsset  24428  fixssdm  24446  fixssrn  24447  funpartss  24482  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  axcontlem10  24601  colinearex  24683  areacirc  24931  dmoprabsss  25033  ducidu  25055  elixp2b  25154  toplat  25290  cntrset  25602  1alg  25722  strded  25739  strcat  25760  cmppar  25973  smbkle  26043  pfsubkl  26047  fneer  26288  neibastop1  26308  neibastop2lem  26309  filnetlem2  26328  filnetlem3  26329  caures  26476  bnd2lem  26515  ismtyres  26532  eldiophb  26836  rencldnfilem  26903  monotuz  27026  fglmod  27171  pwssplit4  27191  dsmmbase  27201  frlmsslsp  27248  pwfi2f1o  27260  mvdco  27388  symgsssg  27408  psgnghm  27437  rabexgf  27695  stoweidlem26  27775  stoweidlem44  27793  stoweidlem50  27799  stoweidlem51  27800  stoweidlem52  27801  stoweidlem57  27806  stoweidlem59  27808  mpt2ndm0  28078  bnj21  28743  bnj1146  28823  bnj1292  28848  bnj1293  28849  bnj1145  29023  bnj1177  29036  toycom  29162  dihglblem2N  31484  lcdvbase  31783  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator