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

Theorem eqsstri 3391
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 3385 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 209 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347
This theorem is referenced by:  eqsstr3i  3392  ssrab2  3442  rabssab  3444  opabss  4358  brab2ga  4917  relopabi  4970  dmopabss  5056  resss  5139  relres  5143  rnin  5251  rnxpss  5275  cnvcnvss  5297  dmmptss  5339  fnres  5532  f0  5597  nfvres  5725  fvopab4ndm  5799  ffvresb  5879  funiunfv  5970  isoini2  6035  ovssunirn  6122  dmoprabss  6177  elmpt2cl  6309  omsson  6485  exse2  6522  fabexg  6538  frxp  6687  mpt2ndm0  6744  tposssxp  6754  dftpos4  6769  smores  6818  smores2  6820  iordsmo  6823  oawordeulem  6998  swoer  7134  swoord1  7135  swoord2  7136  ecss  7147  ecopovsym  7207  ecopovtrn  7208  ecopover  7209  sbthlem7  7432  nnfi  7508  imafi  7609  elfiun  7685  marypha1lem  7688  marypha2lem1  7690  ordtypelem2  7738  hartogslem1  7761  wemapso2OLD  7771  wemapso2lem  7772  wdomima2g  7806  inf3lem1  7839  wemapwe  7933  wemapweOLD  7934  tc2  7967  tz9.12lem1  7999  rankuni  8075  rankuniss  8078  rankmapu  8090  cplem1  8101  hta  8109  r0weon  8184  infxpenlem  8185  ackbij1lem9  8402  ackbij1lem10  8403  ackbij1b  8413  cofsmo  8443  sdom2en01  8476  fin23lem26  8499  fin23lem28  8514  fin23lem30  8516  isf32lem5  8531  isf32lem6  8532  isf32lem7  8533  isf32lem8  8534  fin56  8567  fin1a2lem9  8582  hsmexlem4  8603  hsmexlem5  8604  hsmexlem6  8605  axdc3lem  8624  axdc3lem2  8625  axcclem  8631  zorn2lem1  8670  zorn2lem3  8672  zorn2lem4  8673  zorn2lem5  8674  imadomg  8706  iundom2g  8709  smobeth  8755  canth4  8819  gruina  8990  grur1a  8991  pinn  9052  niex  9055  ltsopi  9062  ltrelpi  9063  dmaddpi  9064  dmmulpi  9065  enqex  9096  0nnq  9098  elpqn  9099  ltrelnq  9100  nqerf  9104  nqerrel  9106  dmrecnq  9142  lterpq  9144  ltrelpr  9172  enrex  9242  ltrelsr  9243  dmaddsr  9257  dmmulsr  9258  ltrelre  9306  axaddf  9317  axmulf  9318  ltrelxr  9443  lerelxr  9445  nn0ssre  10588  nn0ssz  10672  uzsupss  10952  rpnnen1lem1  10984  rpnnen1lem2  10985  rpnnen1lem3  10986  rpnnen1lem5  10988  rpre  11002  uzsup  11707  fzfi  11799  swrd00  12319  sqrlem3  12739  sqrlem5  12741  cau3  12848  caubnd  12851  limsupgre  12964  rlimpm  12983  rlimclim  13029  isercolllem1  13147  isercolllem2  13148  isercoll  13150  caurcvg  13159  caucvg  13161  iseraltlem2  13165  iseraltlem3  13166  zsum  13200  fsumcvg3  13211  climfsum  13288  ackbijnn  13296  infcvgaux1i  13324  dvdszrcl  13545  divalglem2  13604  divalglem5  13606  divalglem8  13609  gcdcllem3  13702  bezoutlem2  13728  bezoutlem3  13729  maxprmfct  13804  phimullem  13859  eulerthlem2  13862  prmdiveq  13866  prmdivdiv  13867  pclem  13910  infpn2  13979  prmreclem2  13983  prmreclem3  13984  prmreclem5  13986  4sqlem1  14014  4sqlem13  14023  4sqlem14  14024  4sqlem17  14027  4sqlem18  14028  4sqlem19  14029  vdwnnlem3  14063  ramcl2lem  14075  ramtcl  14076  ramtcl2  14077  ramtub  14078  ramub1lem2  14093  structcnvcnv  14190  fvsetsid  14204  strlemor0  14269  strlemor1  14270  strleun  14273  imasdsval2  14459  gsumval1  15514  nmzsubg  15727  nmznsg  15730  conjnmz  15785  conjnmzb  15786  gicer  15809  gastacl  15832  symgbasfi  15896  mvdco  15956  symgsssg  15978  sylow1lem2  16103  sylow1lem3  16104  sylow1lem4  16105  sylow1lem5  16106  sylow2a  16123  sylow3lem2  16132  efglem  16218  efgtf  16224  efgtlen  16228  efginvrel2  16229  efginvrel1  16230  efgsfo  16241  efgredlemg  16244  efgredleme  16245  efgredlemd  16246  efgredlemc  16247  efgredlem  16249  efgred  16250  efgrelexlemb  16252  efgcpbllemb  16257  frgpinv  16266  frgpuplem  16274  frgpupf  16275  frgpup1  16277  frgpnabllem2  16357  gsumval3OLD  16387  gsumval3lem1  16388  gsumval3lem2  16389  gsumval3  16390  ablfacrplem  16571  ablfacrp2  16573  ablfac1eu  16579  pgpfaclem1  16587  ablfaclem2  16592  ablfaclem3  16593  lspsolvlem  17228  lbsextlem2  17245  lbsextlem3  17246  lbsextlem4  17247  rrgeq0  17366  rrgss  17369  psrbagconf1o  17449  psrass1lem  17452  mplbasss  17513  ply1bascl  17664  coe1mul2lem2  17727  znf1o  17989  zntoslem  17994  cygznlem2a  18005  psgnghm  18015  pjpm  18138  dsmmbase  18165  frlmsslsp  18228  frlmsslspOLD  18229  mretopd  18701  ordtbas  18801  leordtval2  18821  lecldbas  18828  lmfval  18841  lmbrf  18869  cnconst2  18892  hauscmplem  19014  concompcld  19043  hauspwdom  19110  txuni2  19143  xkouni  19177  xkoccn  19197  txkgen  19230  qtoptop2  19277  kqdisj  19310  hmphtop  19356  hmpher  19362  uzrest  19475  uzfbas  19476  lmflf  19583  ptcmplem1  19629  ptcmplem3  19631  tgpconcompeqg  19687  tgpconcomp  19688  ustn0  19800  imasdsf1olem  19953  xmeter  20013  blcld  20085  isngp2  20194  xrtgioo  20388  iccntr  20403  icccmplem1  20404  icccmplem2  20405  icccmplem3  20406  xmetdcn  20420  metdcn  20422  metdscn2  20438  icchmeo  20518  cnheiborlem  20531  lmmbrf  20778  iscau4  20795  iscauf  20796  caucfil  20799  lmclimf  20819  rrxf  20905  ivthlem1  20940  ivthlem2  20941  ivthlem3  20942  ovolsslem  20972  ovolicc2lem3  21007  ovolicc2lem4  21008  ovolicc2lem5  21009  ovolicc2  21010  volf  21017  uniioombllem3  21070  uniioombllem4  21071  uniioombllem5  21072  dyadmbllem  21084  dyadmbl  21085  volcn  21091  mbfimaopnlem  21138  mbflimsup  21149  i1f1  21173  itg2lcl  21210  iblmbf  21250  itgioo  21298  itgsplitioo  21320  limcflflem  21360  limcflf  21361  limcresi  21365  lhop  21493  dvfsumlem1  21503  dvfsumlem2  21504  dvfsumlem3  21505  dvfsumlem4  21506  dvfsumrlimge0  21507  dvfsumrlim  21508  dvfsumrlim2  21509  dvfsum2  21511  vieta1lem1  21781  vieta1lem2  21782  psercnlem2  21894  psercnlem1  21895  psercn  21896  pserdvlem1  21897  pserdvlem2  21898  pserdv  21899  pserdv2  21900  abelthlem4  21904  abelthlem6  21906  abelthlem9  21910  abelth  21911  logcnlem5  22096  dvlog  22101  dvlog2lem  22102  dvlog2  22103  cxpcn3lem  22190  cxpcn3  22191  sqrcn  22193  1cubr  22242  atansssdm  22333  atancn  22336  jensen  22387  wilthlem1  22411  ftalem3  22417  dvdsflip  22527  musum  22536  dvdsmulf1o  22539  fsumdvdsmul  22540  ppiub  22548  lgsfcl2  22646  lgsquadlem1  22698  lgsquadlem2  22699  lgsquadlem3  22700  2sqlem7  22714  rpvmasum2  22766  dchrisum0re  22767  dchrisum0lema  22768  dchrisum0lem1b  22769  dchrisum0lem1  22770  dchrisum0lem2a  22771  dchrisum0lem2  22772  dchrisum0lem3  22773  dchrisum0  22774  pntlem3  22863  axtgcgrrflx  22928  axtgcgrid  22929  axtgsegcon  22930  axtg5seg  22931  axtgbtwnid  22932  axtgpasch  22933  axtgcont1  22934  tglng  22985  axcontlem2  23216  axcontlem7  23221  axcontlem8  23222  axcontlem10  23224  nbgraf1olem1  23355  issubgoi  23802  flddivrng  23907  phnv  24219  htthlem  24324  hlimadd  24600  hlimcaui  24644  hhsscms  24685  occllem  24711  shjshsi  24900  3oalem4  25073  pjfi  25112  dmadjss  25296  nlelshi  25469  nlelchi  25470  hmopidmchi  25560  atssch  25752  shatomistici  25770  mptctf  26026  fcobijfs  26031  cnre2csqima  26346  raddcn  26364  rrhre  26452  esumsn  26520  sxbrsiga  26710  oddpwdc  26742  eulerpartlem1  26755  eulerpartlemt  26759  eulerpartgbij  26760  eulerpartlemmf  26763  eulerpartlemgvv  26764  eulerpartlemgh  26766  sseqf  26780  ballotlemoex  26873  ballotlemfmpn  26882  ballotth  26925  signswch  26967  lgamucov  27029  lgamucov2  27030  subfacp1lem3  27075  subfacp1lem5  27077  erdszelem2  27085  kur14lem3  27101  kur14lem6  27104  kur14lem7  27105  kur14lem9  27107  cvmlift2lem12  27208  ghomgrpilem2  27310  divcnvshft  27403  clim2prod  27408  ntrivcvg  27417  ntrivcvgfvn0  27419  ntrivcvgtail  27420  ntrivcvgmullem  27421  ntrivcvgmul  27422  zprod  27455  dfpo2  27570  predss  27637  wfrlem7  27735  wlimss  27771  frrlem7  27783  txpss3v  27914  pprodss4v  27920  relsset  27924  fixssdm  27942  fixssrn  27943  limitssson  27947  funpartss  27980  colinearex  28096  dvcncxp1  28482  dvcnsqr  28483  dvasin  28485  dvacos  28486  areacirc  28494  fneer  28565  neibastop1  28585  neibastop2lem  28586  filnetlem2  28605  filnetlem3  28606  caures  28661  bnd2lem  28695  ismtyres  28712  eldiophb  29100  monotuz  29287  fglmod  29431  pwssplit4  29447  pwfi2f1o  29456  arearect  29596  rabexgf  29751  stoweidlem26  29826  stoweidlem44  29844  stoweidlem50  29850  stoweidlem51  29851  stoweidlem52  29852  stoweidlem57  29857  stoweidlem59  29859  disjxwwlkn  30569  clwlknclwlkdifnum  30584  frgrawopreg1  30648  frgrawopreg2  30649  bnj21  31711  bnj1146  31790  bnj1292  31814  bnj1293  31815  bnj1145  31989  bnj1177  32002  bj-tagss  32478  bj-cmnssmnd  32577  bj-ablssgrp  32579  bj-ablsscmn  32581  bj-vecssmod  32584  bj-rrvecssvec  32591  toycom  32623  dihglblem2N  34944  lcdvbase  35243  mapdunirnN  35300
  Copyright terms: Public domain W3C validator