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

Theorem eqsstri 3516
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 3510 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 209 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  eqsstr3i  3517  ssrab2  3567  rabssab  3569  opabss  4494  brab2ga  5061  relopabi  5114  dmopabss  5200  resss  5283  relres  5287  rnin  5401  rnxpss  5425  cnvcnvss  5447  dmmptss  5489  fnres  5683  f0  5752  nfvres  5882  fvopab4ndm  5959  ffvresb  6043  funiunfv  6141  isoini2  6216  ovssunirn  6306  dmoprabss  6365  mpt2ndm0  6497  elmpt2cl  6498  omsson  6685  exse2  6720  fabexg  6737  frxp  6891  tposssxp  6957  dftpos4  6972  smores  7021  smores2  7023  iordsmo  7026  oawordeulem  7201  swoer  7337  swoord1  7338  swoord2  7339  ecss  7351  ecopovsym  7411  ecopovtrn  7412  ecopover  7413  sbthlem7  7631  nnfi  7708  imafi  7811  elfiun  7888  marypha1lem  7891  marypha2lem1  7893  ordtypelem2  7942  hartogslem1  7965  wemapso2OLD  7975  wemapso2lem  7976  wdomima2g  8010  inf3lem1  8043  wemapwe  8137  wemapweOLD  8138  tc2  8171  tz9.12lem1  8203  rankuni  8279  rankuniss  8282  rankmapu  8294  cplem1  8305  hta  8313  r0weon  8388  infxpenlem  8389  ackbij1lem9  8606  ackbij1lem10  8607  ackbij1b  8617  cofsmo  8647  sdom2en01  8680  fin23lem26  8703  fin23lem28  8718  fin23lem30  8720  isf32lem5  8735  isf32lem6  8736  isf32lem7  8737  isf32lem8  8738  fin56  8771  fin1a2lem9  8786  hsmexlem4  8807  hsmexlem5  8808  hsmexlem6  8809  axdc3lem  8828  axdc3lem2  8829  axcclem  8835  zorn2lem1  8874  zorn2lem3  8876  zorn2lem4  8877  zorn2lem5  8878  imadomg  8910  iundom2g  8913  smobeth  8959  canth4  9023  gruina  9194  grur1a  9195  pinn  9254  niex  9257  ltsopi  9264  ltrelpi  9265  dmaddpi  9266  dmmulpi  9267  enqex  9298  0nnq  9300  elpqn  9301  ltrelnq  9302  nqerf  9306  nqerrel  9308  dmrecnq  9344  lterpq  9346  ltrelpr  9374  enrex  9442  ltrelsr  9443  dmaddsr  9460  dmmulsr  9461  ltrelre  9509  axaddf  9520  axmulf  9521  ltrelxr  9646  lerelxr  9648  nn0ssre  10800  nn0ssz  10886  uzsupss  11178  rpnnen1lem1  11212  rpnnen1lem2  11213  rpnnen1lem3  11214  rpnnen1lem5  11216  rpre  11230  uzsup  11964  fzfi  12056  swrd00  12619  sqrlem3  13052  sqrlem5  13054  cau3  13162  caubnd  13165  limsupgre  13278  rlimpm  13297  rlimclim  13343  isercolllem1  13461  isercolllem2  13462  isercoll  13464  caurcvg  13473  caucvg  13475  iseraltlem2  13479  iseraltlem3  13480  zsum  13514  fsumcvg3  13525  climfsum  13608  ackbijnn  13614  infcvgaux1i  13642  dvdszrcl  13863  divalglem2  13925  divalglem5  13927  divalglem8  13930  gcdcllem3  14023  bezoutlem2  14049  bezoutlem3  14050  maxprmfct  14126  phimullem  14181  eulerthlem2  14184  prmdiveq  14188  prmdivdiv  14189  pclem  14234  infpn2  14303  prmreclem2  14307  prmreclem3  14308  prmreclem5  14310  4sqlem1  14338  4sqlem13  14347  4sqlem14  14348  4sqlem17  14351  4sqlem18  14352  4sqlem19  14353  vdwnnlem3  14387  ramcl2lem  14399  ramtcl  14400  ramtcl2  14401  ramtub  14402  ramub1lem2  14417  structcnvcnv  14515  fvsetsid  14529  strlemor0  14595  strlemor1  14596  strleun  14599  imasdsval2  14785  gsumval1  15773  nmzsubg  16111  nmznsg  16114  conjnmz  16169  conjnmzb  16170  gicer  16193  gastacl  16216  symgbasfi  16280  mvdco  16339  symgsssg  16361  sylow1lem2  16488  sylow1lem3  16489  sylow1lem4  16490  sylow1lem5  16491  sylow2a  16508  sylow3lem2  16517  efglem  16603  efgtf  16609  efgtlen  16613  efginvrel2  16614  efginvrel1  16615  efgsfo  16626  efgredlemg  16629  efgredleme  16630  efgredlemd  16631  efgredlemc  16632  efgredlem  16634  efgred  16635  efgrelexlemb  16637  efgcpbllemb  16642  frgpinv  16651  frgpuplem  16659  frgpupf  16660  frgpup1  16662  frgpnabllem2  16747  gsumval3OLD  16777  gsumval3lem1  16778  gsumval3lem2  16779  gsumval3  16780  ablfacrplem  16984  ablfacrp2  16986  ablfac1eu  16992  pgpfaclem1  17000  ablfaclem2  17005  ablfaclem3  17006  lspsolvlem  17656  lbsextlem2  17673  lbsextlem3  17674  lbsextlem4  17675  rrgeq0  17806  rrgss  17809  psrbagconf1o  17894  psrass1lem  17897  mplbasss  17959  ply1bascl  18110  coe1mul2lem2  18177  znf1o  18457  zntoslem  18462  cygznlem2a  18473  psgnghm  18483  pjpm  18606  dsmmbase  18633  frlmsslsp  18696  frlmsslspOLD  18697  mretopd  19459  ordtbas  19559  leordtval2  19579  lecldbas  19586  lmfval  19599  lmbrf  19627  cnconst2  19650  hauscmplem  19772  concompcld  19801  hauspwdom  19868  txuni2  19932  xkouni  19966  xkoccn  19986  txkgen  20019  qtoptop2  20066  kqdisj  20099  hmphtop  20145  hmpher  20151  uzrest  20264  uzfbas  20265  lmflf  20372  ptcmplem1  20418  ptcmplem3  20420  tgpconcompeqg  20476  tgpconcomp  20477  ustn0  20589  imasdsf1olem  20742  xmeter  20802  blcld  20874  isngp2  20983  xrtgioo  21177  iccntr  21192  icccmplem1  21193  icccmplem2  21194  icccmplem3  21195  xmetdcn  21209  metdcn  21211  metdscn2  21227  icchmeo  21307  cnheiborlem  21320  lmmbrf  21567  iscau4  21584  iscauf  21585  caucfil  21588  lmclimf  21608  rrxf  21694  ivthlem1  21729  ivthlem2  21730  ivthlem3  21731  ovolsslem  21761  ovolicc2lem3  21796  ovolicc2lem4  21797  ovolicc2lem5  21798  ovolicc2  21799  volf  21806  uniioombllem3  21860  uniioombllem4  21861  uniioombllem5  21862  dyadmbllem  21874  dyadmbl  21875  volcn  21881  mbfimaopnlem  21928  mbflimsup  21939  i1f1  21963  itg2lcl  22000  iblmbf  22040  itgioo  22088  itgsplitioo  22110  limcflflem  22150  limcflf  22151  limcresi  22155  lhop  22283  dvfsumlem1  22293  dvfsumlem2  22294  dvfsumlem3  22295  dvfsumlem4  22296  dvfsumrlimge0  22297  dvfsumrlim  22298  dvfsumrlim2  22299  dvfsum2  22301  vieta1lem1  22571  vieta1lem2  22572  psercnlem2  22684  psercnlem1  22685  psercn  22686  pserdvlem1  22687  pserdvlem2  22688  pserdv  22689  pserdv2  22690  abelthlem4  22694  abelthlem6  22696  abelthlem9  22700  abelth  22701  logcnlem5  22892  dvlog  22897  dvlog2lem  22898  dvlog2  22899  cxpcn3lem  22986  cxpcn3  22987  sqrtcn  22989  1cubr  23038  atansssdm  23129  atancn  23132  jensen  23183  wilthlem1  23207  ftalem3  23213  dvdsflip  23323  musum  23332  dvdsmulf1o  23335  fsumdvdsmul  23336  ppiub  23344  lgsfcl2  23442  lgsquadlem1  23494  lgsquadlem2  23495  lgsquadlem3  23496  2sqlem7  23510  rpvmasum2  23562  dchrisum0re  23563  dchrisum0lema  23564  dchrisum0lem1b  23565  dchrisum0lem1  23566  dchrisum0lem2a  23567  dchrisum0lem2  23568  dchrisum0lem3  23569  dchrisum0  23570  pntlem3  23659  axtgcgrrflx  23724  axtgcgrid  23725  axtgsegcon  23726  axtg5seg  23727  axtgbtwnid  23728  axtgpasch  23729  axtgcont1  23730  tglng  23798  axcontlem2  24133  axcontlem7  24138  axcontlem8  24139  axcontlem10  24141  nbgraf1olem1  24306  disjxwwlkn  24610  clwlknclwlkdifnum  24826  frgrawopreg1  24915  frgrawopreg2  24916  issubgoi  25177  flddivrng  25282  phnv  25594  htthlem  25699  hlimadd  25975  hlimcaui  26019  hhsscms  26060  occllem  26086  shjshsi  26275  3oalem4  26448  pjfi  26487  dmadjss  26671  nlelshi  26844  nlelchi  26845  hmopidmchi  26935  atssch  27127  shatomistici  27145  fcoinver  27325  mptctf  27409  fcobijfs  27414  cnre2csqima  27759  raddcn  27777  rrhre  27865  esumsn  27938  sxbrsiga  28127  oddpwdc  28159  eulerpartlem1  28172  eulerpartlemt  28176  eulerpartgbij  28177  eulerpartlemmf  28180  eulerpartlemgvv  28181  eulerpartlemgh  28183  sseqf  28197  ballotlemfmpn  28299  ballotth  28342  signswch  28384  lgamucov  28446  lgamucov2  28447  subfacp1lem3  28492  subfacp1lem5  28494  erdszelem2  28502  kur14lem3  28518  kur14lem6  28521  kur14lem7  28522  kur14lem9  28524  cvmlift2lem12  28625  mpstssv  28765  mstapst  28773  mppspstlem  28797  mppspst  28800  mthmsta  28804  mthmpps  28808  mclsppslem  28809  ghomgrpilem2  28892  divcnvshft  28985  clim2prod  28990  ntrivcvg  28999  ntrivcvgfvn0  29001  ntrivcvgtail  29002  ntrivcvgmullem  29003  ntrivcvgmul  29004  zprod  29037  dfpo2  29152  predss  29219  wfrlem7  29317  wlimss  29353  frrlem7  29365  txpss3v  29496  pprodss4v  29502  relsset  29506  fixssdm  29524  fixssrn  29525  limitssson  29529  funpartss  29562  colinearex  29678  dvcncxp1  30068  dvcnsqrt  30069  dvasin  30071  dvacos  30072  areacirc  30080  fneer  30139  neibastop1  30145  neibastop2lem  30146  filnetlem2  30165  filnetlem3  30166  caures  30221  bnd2lem  30255  ismtyres  30272  eldiophb  30658  monotuz  30845  fglmod  30987  pwssplit4  31003  pwfi2f1o  31012  arearect  31152  rabexgf  31346  limcperiod  31538  sumnnodd  31540  cncfshift  31579  cncfperiod  31584  ibliooicc  31656  stoweidlem26  31693  stoweidlem44  31711  stoweidlem50  31717  stoweidlem51  31718  stoweidlem52  31719  stoweidlem57  31724  stoweidlem59  31726  fourierdlem16  31790  fourierdlem19  31793  fourierdlem21  31795  fourierdlem22  31796  fourierdlem42  31816  fourierdlem83  31857  fouriersw  31899  oddibas  32334  2zlidl  32440  2zrngbas  32442  2zrng0  32444  fldc  32599  fldhmsubc  32600  fldcOLD  32618  fldhmsubcOLD  32619  bnj21  33478  bnj1146  33557  bnj1292  33581  bnj1293  33582  bnj1145  33756  bnj1177  33769  bj-tagss  34250  bj-cmnssmnd  34354  bj-ablssgrp  34356  bj-ablsscmn  34358  bj-vecssmod  34361  bj-rrvecssvec  34368  toycom  34400  dihglblem2N  36723  lcdvbase  37022  mapdunirnN  37079  rp-imass  37444
  Copyright terms: Public domain W3C validator