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

Theorem eqsstri 3534
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 3528 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 209 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  eqsstr3i  3535  ssrab2  3585  rabssab  3587  opabss  4508  brab2ga  5073  relopabi  5126  dmopabss  5212  resss  5295  relres  5299  rnin  5413  rnxpss  5437  cnvcnvss  5459  dmmptss  5501  fnres  5695  f0  5764  nfvres  5894  fvopab4ndm  5970  ffvresb  6050  funiunfv  6146  isoini2  6221  ovssunirn  6308  dmoprabss  6366  mpt2ndm0  6498  elmpt2cl  6499  omsson  6682  exse2  6720  fabexg  6737  frxp  6890  tposssxp  6956  dftpos4  6971  smores  7020  smores2  7022  iordsmo  7025  oawordeulem  7200  swoer  7336  swoord1  7337  swoord2  7338  ecss  7350  ecopovsym  7410  ecopovtrn  7411  ecopover  7412  sbthlem7  7630  nnfi  7707  imafi  7809  elfiun  7886  marypha1lem  7889  marypha2lem1  7891  ordtypelem2  7940  hartogslem1  7963  wemapso2OLD  7973  wemapso2lem  7974  wdomima2g  8008  inf3lem1  8041  wemapwe  8135  wemapweOLD  8136  tc2  8169  tz9.12lem1  8201  rankuni  8277  rankuniss  8280  rankmapu  8292  cplem1  8303  hta  8311  r0weon  8386  infxpenlem  8387  ackbij1lem9  8604  ackbij1lem10  8605  ackbij1b  8615  cofsmo  8645  sdom2en01  8678  fin23lem26  8701  fin23lem28  8716  fin23lem30  8718  isf32lem5  8733  isf32lem6  8734  isf32lem7  8735  isf32lem8  8736  fin56  8769  fin1a2lem9  8784  hsmexlem4  8805  hsmexlem5  8806  hsmexlem6  8807  axdc3lem  8826  axdc3lem2  8827  axcclem  8833  zorn2lem1  8872  zorn2lem3  8874  zorn2lem4  8875  zorn2lem5  8876  imadomg  8908  iundom2g  8911  smobeth  8957  canth4  9021  gruina  9192  grur1a  9193  pinn  9252  niex  9255  ltsopi  9262  ltrelpi  9263  dmaddpi  9264  dmmulpi  9265  enqex  9296  0nnq  9298  elpqn  9299  ltrelnq  9300  nqerf  9304  nqerrel  9306  dmrecnq  9342  lterpq  9344  ltrelpr  9372  enrex  9440  ltrelsr  9441  dmaddsr  9458  dmmulsr  9459  ltrelre  9507  axaddf  9518  axmulf  9519  ltrelxr  9644  lerelxr  9646  nn0ssre  10795  nn0ssz  10881  uzsupss  11170  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  rpre  11222  uzsup  11954  fzfi  12046  swrd00  12604  sqrlem3  13037  sqrlem5  13039  cau3  13147  caubnd  13150  limsupgre  13263  rlimpm  13282  rlimclim  13328  isercolllem1  13446  isercolllem2  13447  isercoll  13449  caurcvg  13458  caucvg  13460  iseraltlem2  13464  iseraltlem3  13465  zsum  13499  fsumcvg3  13510  climfsum  13593  ackbijnn  13599  infcvgaux1i  13627  dvdszrcl  13848  divalglem2  13908  divalglem5  13910  divalglem8  13913  gcdcllem3  14006  bezoutlem2  14032  bezoutlem3  14033  maxprmfct  14109  phimullem  14164  eulerthlem2  14167  prmdiveq  14171  prmdivdiv  14172  pclem  14217  infpn2  14286  prmreclem2  14290  prmreclem3  14291  prmreclem5  14293  4sqlem1  14321  4sqlem13  14330  4sqlem14  14331  4sqlem17  14334  4sqlem18  14335  4sqlem19  14336  vdwnnlem3  14370  ramcl2lem  14382  ramtcl  14383  ramtcl2  14384  ramtub  14385  ramub1lem2  14400  structcnvcnv  14497  fvsetsid  14511  strlemor0  14577  strlemor1  14578  strleun  14581  imasdsval2  14767  gsumval1  15822  nmzsubg  16037  nmznsg  16040  conjnmz  16095  conjnmzb  16096  gicer  16119  gastacl  16142  symgbasfi  16206  mvdco  16266  symgsssg  16288  sylow1lem2  16415  sylow1lem3  16416  sylow1lem4  16417  sylow1lem5  16418  sylow2a  16435  sylow3lem2  16444  efglem  16530  efgtf  16536  efgtlen  16540  efginvrel2  16541  efginvrel1  16542  efgsfo  16553  efgredlemg  16556  efgredleme  16557  efgredlemd  16558  efgredlemc  16559  efgredlem  16561  efgred  16562  efgrelexlemb  16564  efgcpbllemb  16569  frgpinv  16578  frgpuplem  16586  frgpupf  16587  frgpup1  16589  frgpnabllem2  16669  gsumval3OLD  16699  gsumval3lem1  16700  gsumval3lem2  16701  gsumval3  16702  ablfacrplem  16906  ablfacrp2  16908  ablfac1eu  16914  pgpfaclem1  16922  ablfaclem2  16927  ablfaclem3  16928  lspsolvlem  17571  lbsextlem2  17588  lbsextlem3  17589  lbsextlem4  17590  rrgeq0  17709  rrgss  17712  psrbagconf1o  17797  psrass1lem  17800  mplbasss  17862  ply1bascl  18013  coe1mul2lem2  18080  znf1o  18357  zntoslem  18362  cygznlem2a  18373  psgnghm  18383  pjpm  18506  dsmmbase  18533  frlmsslsp  18596  frlmsslspOLD  18597  mretopd  19359  ordtbas  19459  leordtval2  19479  lecldbas  19486  lmfval  19499  lmbrf  19527  cnconst2  19550  hauscmplem  19672  concompcld  19701  hauspwdom  19768  txuni2  19801  xkouni  19835  xkoccn  19855  txkgen  19888  qtoptop2  19935  kqdisj  19968  hmphtop  20014  hmpher  20020  uzrest  20133  uzfbas  20134  lmflf  20241  ptcmplem1  20287  ptcmplem3  20289  tgpconcompeqg  20345  tgpconcomp  20346  ustn0  20458  imasdsf1olem  20611  xmeter  20671  blcld  20743  isngp2  20852  xrtgioo  21046  iccntr  21061  icccmplem1  21062  icccmplem2  21063  icccmplem3  21064  xmetdcn  21078  metdcn  21080  metdscn2  21096  icchmeo  21176  cnheiborlem  21189  lmmbrf  21436  iscau4  21453  iscauf  21454  caucfil  21457  lmclimf  21477  rrxf  21563  ivthlem1  21598  ivthlem2  21599  ivthlem3  21600  ovolsslem  21630  ovolicc2lem3  21665  ovolicc2lem4  21666  ovolicc2lem5  21667  ovolicc2  21668  volf  21675  uniioombllem3  21729  uniioombllem4  21730  uniioombllem5  21731  dyadmbllem  21743  dyadmbl  21744  volcn  21750  mbfimaopnlem  21797  mbflimsup  21808  i1f1  21832  itg2lcl  21869  iblmbf  21909  itgioo  21957  itgsplitioo  21979  limcflflem  22019  limcflf  22020  limcresi  22024  lhop  22152  dvfsumlem1  22162  dvfsumlem2  22163  dvfsumlem3  22164  dvfsumlem4  22165  dvfsumrlimge0  22166  dvfsumrlim  22167  dvfsumrlim2  22168  dvfsum2  22170  vieta1lem1  22440  vieta1lem2  22441  psercnlem2  22553  psercnlem1  22554  psercn  22555  pserdvlem1  22556  pserdvlem2  22557  pserdv  22558  pserdv2  22559  abelthlem4  22563  abelthlem6  22565  abelthlem9  22569  abelth  22570  logcnlem5  22755  dvlog  22760  dvlog2lem  22761  dvlog2  22762  cxpcn3lem  22849  cxpcn3  22850  sqrtcn  22852  1cubr  22901  atansssdm  22992  atancn  22995  jensen  23046  wilthlem1  23070  ftalem3  23076  dvdsflip  23186  musum  23195  dvdsmulf1o  23198  fsumdvdsmul  23199  ppiub  23207  lgsfcl2  23305  lgsquadlem1  23357  lgsquadlem2  23358  lgsquadlem3  23359  2sqlem7  23373  rpvmasum2  23425  dchrisum0re  23426  dchrisum0lema  23427  dchrisum0lem1b  23428  dchrisum0lem1  23429  dchrisum0lem2a  23430  dchrisum0lem2  23431  dchrisum0lem3  23432  dchrisum0  23433  pntlem3  23522  axtgcgrrflx  23587  axtgcgrid  23588  axtgsegcon  23589  axtg5seg  23590  axtgbtwnid  23591  axtgpasch  23592  axtgcont1  23593  tglng  23661  axcontlem2  23944  axcontlem7  23949  axcontlem8  23950  axcontlem10  23952  nbgraf1olem1  24117  disjxwwlkn  24421  clwlknclwlkdifnum  24637  frgrawopreg1  24727  frgrawopreg2  24728  issubgoi  24988  flddivrng  25093  phnv  25405  htthlem  25510  hlimadd  25786  hlimcaui  25830  hhsscms  25871  occllem  25897  shjshsi  26086  3oalem4  26259  pjfi  26298  dmadjss  26482  nlelshi  26655  nlelchi  26656  hmopidmchi  26746  atssch  26938  shatomistici  26956  fcoinver  27133  mptctf  27216  fcobijfs  27221  cnre2csqima  27529  raddcn  27547  rrhre  27635  esumsn  27712  sxbrsiga  27901  oddpwdc  27933  eulerpartlem1  27946  eulerpartlemt  27950  eulerpartgbij  27951  eulerpartlemmf  27954  eulerpartlemgvv  27955  eulerpartlemgh  27957  sseqf  27971  ballotlemoex  28064  ballotlemfmpn  28073  ballotth  28116  signswch  28158  lgamucov  28220  lgamucov2  28221  subfacp1lem3  28266  subfacp1lem5  28268  erdszelem2  28276  kur14lem3  28292  kur14lem6  28295  kur14lem7  28296  kur14lem9  28298  cvmlift2lem12  28399  ghomgrpilem2  28501  divcnvshft  28594  clim2prod  28599  ntrivcvg  28608  ntrivcvgfvn0  28610  ntrivcvgtail  28611  ntrivcvgmullem  28612  ntrivcvgmul  28613  zprod  28646  dfpo2  28761  predss  28828  wfrlem7  28926  wlimss  28962  frrlem7  28974  txpss3v  29105  pprodss4v  29111  relsset  29115  fixssdm  29133  fixssrn  29134  limitssson  29138  funpartss  29171  colinearex  29287  dvcncxp1  29677  dvcnsqrt  29678  dvasin  29680  dvacos  29681  areacirc  29689  fneer  29760  neibastop1  29780  neibastop2lem  29781  filnetlem2  29800  filnetlem3  29801  caures  29856  bnd2lem  29890  ismtyres  29907  eldiophb  30294  monotuz  30481  fglmod  30623  pwssplit4  30639  pwfi2f1o  30648  arearect  30788  rabexgf  30977  limcperiod  31170  sumnnodd  31172  cncfshift  31212  cncfperiod  31217  ibliooicc  31289  stoweidlem26  31326  stoweidlem44  31344  stoweidlem50  31350  stoweidlem51  31351  stoweidlem52  31352  stoweidlem57  31357  stoweidlem59  31359  fourierdlem16  31423  fourierdlem19  31426  fourierdlem21  31428  fourierdlem22  31429  fourierdlem42  31449  fourierdlem83  31490  fouriersw  31532  bnj21  32850  bnj1146  32929  bnj1292  32953  bnj1293  32954  bnj1145  33128  bnj1177  33141  bj-tagss  33619  bj-cmnssmnd  33724  bj-ablssgrp  33726  bj-ablsscmn  33728  bj-vecssmod  33731  bj-rrvecssvec  33738  toycom  33770  dihglblem2N  36091  lcdvbase  36390  mapdunirnN  36447  rp-imass  36796
  Copyright terms: Public domain W3C validator