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

Theorem eqsstri 3500
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 3494 . 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 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  eqsstr3i  3501  ssrab2  3552  rabssab  3554  opabss  4487  brab2ga  4930  relopabi  4979  dmopabss  5066  resss  5148  relres  5152  rnin  5265  rnxpss  5289  cnvcnvss  5310  dmmptss  5351  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  6985  dftpos4  7000  wfrdmss  7050  smores  7079  smores2  7081  iordsmo  7084  oawordeulem  7263  swoer  7399  swoord1  7400  swoord2  7401  ecss  7413  ecopovsym  7473  ecopovtrn  7474  ecopover  7475  sbthlem7  7694  nnfi  7771  imafi  7873  elfiun  7950  marypha1lem  7953  marypha2lem1  7955  ordtypelem2  8034  hartogslem1  8057  wemapso2lem  8067  wdomima2g  8101  inf3lem1  8133  wemapwe  8201  tc2  8225  tz9.12lem1  8257  rankuni  8333  rankuniss  8336  rankmapu  8348  cplem1  8359  hta  8367  r0weon  8442  infxpenlem  8443  ackbij1lem9  8656  ackbij1lem10  8657  ackbij1b  8667  cofsmo  8697  sdom2en01  8730  fin23lem26  8753  fin23lem28  8768  fin23lem30  8770  isf32lem5  8785  isf32lem6  8786  isf32lem7  8787  isf32lem8  8788  fin56  8821  fin1a2lem9  8836  hsmexlem4  8857  hsmexlem5  8858  hsmexlem6  8859  axdc3lem  8878  axdc3lem2  8879  axcclem  8885  zorn2lem1  8924  zorn2lem3  8926  zorn2lem4  8927  zorn2lem5  8928  imadomg  8960  iundom2g  8963  smobeth  9009  canth4  9071  gruina  9242  grur1a  9243  pinn  9302  niex  9305  ltsopi  9312  ltrelpi  9313  dmaddpi  9314  dmmulpi  9315  enqex  9346  0nnq  9348  elpqn  9349  ltrelnq  9350  nqerf  9354  nqerrel  9356  dmrecnq  9392  lterpq  9394  ltrelpr  9422  enrex  9490  ltrelsr  9491  dmaddsr  9508  dmmulsr  9509  ltrelre  9557  axaddf  9568  axmulf  9569  ltrelxr  9694  lerelxr  9696  nn0ssre  10873  nn0ssz  10958  uzsupss  11256  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  rpre  11308  uzsup  12087  fzfi  12182  swrd00  12759  sqrlem3  13287  sqrlem5  13289  cau3  13397  caubnd  13400  limsupgre  13520  limsupgreOLD  13521  rlimpm  13542  rlimclim  13588  isercolllem1  13706  isercolllem2  13707  isercoll  13709  caurcvg  13720  caurcvgOLD  13721  caucvg  13723  iseraltlem2  13727  iseraltlem3  13728  zsum  13762  fsumcvg3  13773  climfsum  13858  ackbijnn  13864  divcnvshft  13891  infcvgaux1i  13893  clim2prod  13922  ntrivcvg  13931  ntrivcvgfvn0  13933  ntrivcvgtail  13934  ntrivcvgmullem  13935  ntrivcvgmul  13936  zprod  13969  dvdszrcl  14288  divalglem2  14351  divalglem5  14353  divalglem8  14356  gcdcllem3  14449  bezoutlem2  14478  bezoutlem3  14479  maxprmfct  14623  phimullem  14696  eulerthlem2  14699  prmdiveq  14703  prmdivdiv  14704  pclem  14751  infpn2  14820  prmreclem2  14824  prmreclem3  14825  prmreclem5  14827  4sqlem1  14855  4sqlem13OLD  14864  4sqlem14OLD  14865  4sqlem17OLD  14868  4sqlem18OLD  14869  4sqlem13  14870  4sqlem14  14871  4sqlem17  14874  4sqlem18  14875  4sqlem19  14876  vdwnnlem3  14910  ramcl2lem  14925  ramcl2lemOLD  14926  ramtcl  14927  ramtclOLD  14928  ramtcl2  14929  ramtcl2OLD  14930  ramtub  14931  ramtubOLD  14932  ramub1lem2  14948  structcnvcnv  15095  fvsetsid  15111  strlemor0  15178  strlemor1  15179  strleun  15182  imasdsval2  15373  gsumval1  16471  nmzsubg  16809  nmznsg  16812  conjnmz  16867  conjnmzb  16868  gicer  16891  gastacl  16914  symgbasfi  16978  mvdco  17037  symgsssg  17059  sylow1lem2  17186  sylow1lem3  17187  sylow1lem4  17188  sylow1lem5  17189  sylow2a  17206  sylow3lem2  17215  efglem  17301  efgtf  17307  efgtlen  17311  efginvrel2  17312  efginvrel1  17313  efgsfo  17324  efgredlemg  17327  efgredleme  17328  efgredlemd  17329  efgredlemc  17330  efgredlem  17332  efgred  17333  efgrelexlemb  17335  efgcpbllemb  17340  frgpinv  17349  frgpuplem  17357  frgpupf  17358  frgpup1  17360  frgpnabllem2  17445  gsumval3lem1  17474  gsumval3lem2  17475  gsumval3  17476  ablfacrplem  17633  ablfacrp2  17635  ablfac1eu  17641  pgpfaclem1  17649  ablfaclem2  17654  ablfaclem3  17655  lspsolvlem  18300  lbsextlem2  18317  lbsextlem3  18318  lbsextlem4  18319  rrgeq0  18449  rrgss  18451  psrbagconf1o  18533  psrass1lem  18536  mplbasss  18591  ply1bascl  18731  coe1mul2lem2  18796  znf1o  19053  zntoslem  19058  cygznlem2a  19069  psgnghm  19079  pjpm  19202  dsmmbase  19229  frlmsslsp  19285  mretopd  20039  ordtbas  20139  leordtval2  20159  lecldbas  20166  lmfval  20179  lmbrf  20207  cnconst2  20230  hauscmplem  20352  concompcld  20380  hauspwdom  20447  txuni2  20511  xkouni  20545  xkoccn  20565  txkgen  20598  qtoptop2  20645  kqdisj  20678  hmphtop  20724  hmpher  20730  uzrest  20843  uzfbas  20844  lmflf  20951  ptcmplem1  20998  ptcmplem3  21000  tgpconcompeqg  21057  tgpconcomp  21058  ustn0  21166  imasdsf1olem  21319  xmeter  21379  blcld  21451  isngp2  21542  xrtgioo  21735  iccntr  21750  icccmplem1  21751  icccmplem2  21752  icccmplem3  21753  xmetdcn  21767  metdcn  21769  metdscn2  21785  icchmeo  21865  cnheiborlem  21878  lmmbrf  22125  iscau4  22142  iscauf  22143  caucfil  22146  lmclimf  22166  rrxf  22248  ivthlem1  22283  ivthlem2  22284  ivthlem3  22285  ovolsslem  22315  ovolicc2lem3  22350  ovolicc2lem4  22351  ovolicc2lem5  22352  ovolicc2  22353  volf  22360  uniioombllem3  22420  uniioombllem4  22421  uniioombllem5  22422  dyadmbllem  22434  dyadmbl  22435  volcn  22441  mbfimaopnlem  22488  mbflimsup  22500  mbflimsupOLD  22501  i1f1  22525  itg2lcl  22562  iblmbf  22602  itgioo  22650  itgsplitioo  22672  limcflflem  22712  limcflf  22713  limcresi  22717  lhop  22845  dvfsumlem1  22855  dvfsumlem2  22856  dvfsumlem3  22857  dvfsumlem4  22858  dvfsumrlimge0  22859  dvfsumrlim  22860  dvfsumrlim2  22861  dvfsum2  22863  vieta1lem1  23131  vieta1lem2  23132  psercnlem2  23244  psercnlem1  23245  psercn  23246  pserdvlem1  23247  pserdvlem2  23248  pserdv  23249  pserdv2  23250  abelthlem4  23254  abelthlem6  23256  abelthlem9  23260  abelth  23261  logcnlem5  23456  dvlog  23461  dvlog2lem  23462  dvlog2  23463  dvcncxp1  23548  dvcnsqrt  23549  cxpcn3lem  23552  cxpcn3  23553  sqrtcn  23555  1cubr  23633  atansssdm  23724  atancn  23727  jensen  23779  lgamucov  23828  lgamucov2  23829  wilthlem1  23858  ftalem3  23864  dvdsflip  23974  musum  23983  dvdsmulf1o  23986  fsumdvdsmul  23987  ppiub  23995  lgsfcl2  24093  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  2sqlem7  24161  rpvmasum2  24213  dchrisum0re  24214  dchrisum0lema  24215  dchrisum0lem1b  24216  dchrisum0lem1  24217  dchrisum0lem2a  24218  dchrisum0lem2  24219  dchrisum0lem3  24220  dchrisum0  24221  pntlem3  24310  axtgcgrrflx  24373  axtgcgrid  24374  axtgsegcon  24375  axtg5seg  24376  axtgbtwnid  24377  axtgpasch  24378  axtgcont1  24379  tglng  24451  axcontlem2  24841  axcontlem7  24846  axcontlem8  24847  axcontlem10  24849  nbgraf1olem1  25014  disjxwwlkn  25318  clwlknclwlkdifnum  25534  frgrawopreg1  25623  frgrawopreg2  25624  issubgoi  25883  flddivrng  25988  phnv  26300  htthlem  26405  hlimadd  26681  hlimcaui  26724  hhsscms  26765  occllem  26791  shjshsi  26980  3oalem4  27153  pjfi  27192  dmadjss  27375  nlelshi  27548  nlelchi  27549  hmopidmchi  27639  atssch  27831  shatomistici  27849  fcoinver  28053  mptexgf  28065  mptctf  28148  fcobijfs  28154  psgnfzto1stlem  28452  cnre2csqima  28556  raddcn  28574  rrhre  28664  esumsnf  28724  sxbrsiga  28951  omssubadd  28961  carsggect  28979  oddpwdc  29013  eulerpartlem1  29026  eulerpartlemt  29030  eulerpartgbij  29031  eulerpartlemmf  29034  eulerpartlemgvv  29035  eulerpartlemgh  29037  sseqf  29051  ballotlemfmpn  29153  ballotth  29196  signswch  29238  bnj21  29311  bnj1146  29391  bnj1292  29415  bnj1293  29416  bnj1145  29590  bnj1177  29603  subfacp1lem3  29693  subfacp1lem5  29695  erdszelem2  29703  kur14lem3  29719  kur14lem6  29722  kur14lem7  29723  kur14lem9  29725  cvmlift2lem12  29825  mpstssv  29965  mstapst  29973  mppspstlem  29997  mppspst  30000  mthmsta  30004  mthmpps  30008  mclsppslem  30009  ghomgrpilem2  30092  dfpo2  30182  wlimss  30299  frrlem7  30311  txpss3v  30430  pprodss4v  30436  relsset  30440  fixssdm  30458  fixssrn  30459  limitssson  30463  funpartss  30496  colinearex  30612  fneer  30794  neibastop1  30800  neibastop2lem  30801  filnetlem2  30820  filnetlem3  30821  bj-tagss  31323  bj-cmnssmnd  31436  bj-ablssgrp  31438  bj-ablsscmn  31440  bj-vecssmod  31443  bj-rrvecssvec  31450  icoreresf  31489  icoreunrn  31496  poimirlem29  31672  poimirlem30  31673  poimirlem31  31674  poimir  31676  broucube  31677  dvasin  31731  dvacos  31732  areacirc  31740  caures  31792  bnd2lem  31826  ismtyres  31843  toycom  32247  dihglblem2N  34570  lcdvbase  34869  mapdunirnN  34926  eldiophb  35307  monotuz  35494  fglmod  35636  pwssplit4  35652  pwfi2f1o  35659  arearect  35798  dfrcl2  35904  comptiunov2i  35936  corclrcl  35937  trclrelexplem  35941  relexpaddss  35948  cotrcltrcl  35955  corcltrcl  35969  cotrclrcl  35972  frege131d  35994  rp-imass  36002  xpheOLD  36013  0he  36014  uzmptshftfval  36331  binomcxplemdvbinom  36338  binomcxplemdvsum  36340  binomcxplemnotnn0  36341  rabexgf  36984  uzct  37045  disjf1o  37088  fz1ssfz0  37136  uzfissfz  37157  limcperiod  37279  sumnnodd  37281  cncfshift  37322  cncfperiod  37327  ibliooicc  37416  stoweidlem26  37454  stoweidlem44  37473  stoweidlem50  37479  stoweidlem51  37480  stoweidlem52  37481  stoweidlem57  37486  stoweidlem59  37488  fourierdlem16  37553  fourierdlem19  37556  fourierdlem21  37558  fourierdlem22  37559  fourierdlem42  37579  fourierdlem83  37620  fouriersw  37662  sge0less  37767  sge0fodjrnlem  37791  oddibas  38570  2zlidl  38691  2zrngbas  38693  2zrng0  38695  fldc  38842  fldhmsubc  38843  fldcALTV  38861  fldhmsubcALTV  38862
  Copyright terms: Public domain W3C validator