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

Theorem eqsstri 3338
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 3332 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 201 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    C_ wss 3280
This theorem is referenced by:  eqsstr3i  3339  ssrab2  3388  rabssab  3390  opabss  4229  omsson  4808  brab2ga  4910  relopabi  4959  dmopabss  5040  resss  5129  relres  5133  exse2  5197  rnin  5240  rnxpss  5260  cnvcnvss  5284  dmmptss  5325  fnres  5520  fabexg  5583  f0  5586  nfvres  5719  fvopab4ndm  5784  ffvresb  5859  funiunfv  5954  isoini2  6018  ovssunirn  6066  dmoprabss  6114  elmpt2cl  6247  frxp  6415  mpt2ndm0  6432  tposssxp  6442  dftpos4  6457  smores  6573  smores2  6575  iordsmo  6578  oawordeulem  6756  swoer  6892  swoord1  6893  swoord2  6894  ecss  6905  ecopovsym  6965  ecopovtrn  6966  ecopover  6967  sbthlem7  7182  nnfi  7258  imafi  7357  elfiun  7393  marypha1lem  7396  marypha2lem1  7398  ordtypelem2  7444  hartogslem1  7467  wemapso2  7477  wdomima2g  7510  inf3lem1  7539  cantnfres  7589  wemapwe  7610  tc2  7637  tz9.12lem1  7669  rankuni  7745  rankuniss  7748  cplem1  7769  hta  7777  r0weon  7850  infxpenlem  7851  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1b  8075  cofsmo  8105  sdom2en01  8138  fin23lem26  8161  fin23lem28  8176  fin23lem30  8178  isf32lem5  8193  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  fin56  8229  fin1a2lem9  8244  hsmexlem4  8265  hsmexlem5  8266  hsmexlem6  8267  axdc3lem  8286  axdc3lem2  8287  axcclem  8293  zorn2lem1  8332  zorn2lem3  8334  zorn2lem4  8335  zorn2lem5  8336  imadomg  8368  iundom2g  8371  smobeth  8417  canth4  8478  gruina  8649  grur1a  8650  pinn  8711  niex  8714  ltsopi  8721  ltrelpi  8722  dmaddpi  8723  dmmulpi  8724  enqex  8755  0nnq  8757  elpqn  8758  ltrelnq  8759  nqerf  8763  nqerrel  8765  dmrecnq  8801  lterpq  8803  ltrelpr  8831  enrex  8901  ltrelsr  8902  dmaddsr  8916  dmmulsr  8917  ltrelre  8965  axaddf  8976  axmulf  8977  ltrelxr  9095  lerelxr  9097  nn0ssre  10181  nn0ssz  10258  uzsupss  10524  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  rpre  10574  uzsup  11199  fzfi  11266  swrd00  11720  sqrlem3  12005  sqrlem5  12007  cau3  12114  caubnd  12117  limsupgre  12230  rlimpm  12249  rlimclim  12295  isercolllem1  12413  isercolllem2  12414  isercoll  12416  caurcvg  12425  caucvg  12427  iseraltlem2  12431  iseraltlem3  12432  zsum  12467  fsumcvg3  12478  climfsum  12554  ackbijnn  12562  infcvgaux1i  12591  dvdszrcl  12812  divalglem2  12870  divalglem5  12872  divalglem8  12875  gcdcllem3  12968  bezoutlem2  12994  bezoutlem3  12995  maxprmfct  13068  phimullem  13123  eulerthlem2  13126  prmdiveq  13130  prmdivdiv  13131  pclem  13167  infpn2  13236  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  4sqlem1  13271  4sqlem13  13280  4sqlem14  13281  4sqlem17  13284  4sqlem18  13285  4sqlem19  13286  vdwnnlem3  13320  ramcl2lem  13332  ramtcl  13333  ramtcl2  13334  ramtub  13335  ramub1lem2  13350  structcnvcnv  13435  strlemor0  13510  strlemor1  13511  strleun  13514  imasdsval2  13697  gsumval1  14734  nmzsubg  14936  nmznsg  14939  conjnmz  14994  conjnmzb  14995  gicer  15018  gastacl  15041  sylow1lem2  15188  sylow1lem3  15189  sylow1lem4  15190  sylow1lem5  15191  sylow2a  15208  sylow3lem2  15217  efglem  15303  efgtf  15309  efgtlen  15313  efginvrel2  15314  efginvrel1  15315  efgsfo  15326  efgredlemg  15329  efgredleme  15330  efgredlemd  15331  efgredlemc  15332  efgredlem  15334  efgred  15335  efgrelexlemb  15337  efgcpbllemb  15342  frgpinv  15351  frgpuplem  15359  frgpupf  15360  frgpup1  15362  frgpnabllem2  15440  gsumval3  15469  ablfacrplem  15578  ablfacrp2  15580  ablfac1eu  15586  pgpfaclem1  15594  ablfaclem2  15599  ablfaclem3  15600  lspsolvlem  16169  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  rrgeq0  16305  rrgss  16307  psrbagconf1o  16394  psrass1lem  16397  mplbasss  16451  ply1bascl  16556  coe1mul2lem2  16616  znf1o  16787  zntoslem  16792  cygznlem2a  16803  pjpm  16890  mretopd  17111  ordtbas  17210  leordtval2  17230  lecldbas  17237  lmfval  17250  lmbrf  17278  cnconst2  17301  hauscmplem  17423  concompcld  17450  hauspwdom  17517  txuni2  17550  xkouni  17584  xkoccn  17604  txkgen  17637  qtoptop2  17684  kqdisj  17717  hmphtop  17763  hmpher  17769  uzrest  17882  uzfbas  17883  lmflf  17990  ptcmplem1  18036  ptcmplem3  18038  tgpconcompeqg  18094  tgpconcomp  18095  ustn0  18203  imasdsf1olem  18356  xmeter  18416  blcld  18488  isngp2  18597  xrtgioo  18790  iccntr  18805  icccmplem1  18806  icccmplem2  18807  icccmplem3  18808  xmetdcn  18822  metdcn  18824  metdscn2  18840  icchmeo  18919  cnheiborlem  18932  lmmbrf  19168  iscau4  19185  iscauf  19186  caucfil  19189  lmclimf  19209  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ovolsslem  19333  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ovolicc2  19371  volf  19378  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  dyadmbllem  19444  dyadmbl  19445  volcn  19451  mbfimaopnlem  19500  mbflimsup  19511  i1f1  19535  itg2lcl  19572  iblmbf  19612  itgioo  19660  itgsplitioo  19682  limcflflem  19720  limcflf  19721  limcresi  19725  lhop  19853  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlimge0  19867  dvfsumrlim  19868  dvfsumrlim2  19869  dvfsum2  19871  vieta1lem1  20180  vieta1lem2  20181  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  pserdv2  20299  abelthlem4  20303  abelthlem6  20305  abelthlem9  20309  abelth  20310  logcnlem5  20490  dvlog  20495  dvlog2lem  20496  dvlog2  20497  cxpcn3lem  20584  cxpcn3  20585  sqrcn  20587  1cubr  20635  atansssdm  20726  atancn  20729  jensen  20780  wilthlem1  20804  ftalem3  20810  dvdsflip  20920  musum  20929  dvdsmulf1o  20932  fsumdvdsmul  20933  ppiub  20941  lgsfcl2  21039  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  2sqlem7  21107  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrisum0  21167  pntlem3  21256  nbgraf1olem1  21404  issubgoi  21851  flddivrng  21956  phnv  22268  htthlem  22373  hlimadd  22648  hlimcaui  22692  hhsscms  22732  occllem  22758  shjshsi  22947  3oalem4  23120  pjfi  23159  dmadjss  23343  nlelshi  23516  nlelchi  23517  hmopidmchi  23607  atssch  23799  shatomistici  23817  mptctf  24065  cnre2csqima  24262  raddcn  24268  rrhre  24340  esumsn  24409  sxbrsiga  24593  sitmcl  24616  ballotlemoex  24696  ballotlemfmpn  24705  ballotth  24748  lgamucov  24775  lgamucov2  24776  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem2  24831  kur14lem3  24847  kur14lem6  24850  kur14lem7  24851  kur14lem9  24853  cvmlift2lem12  24954  ghomgrpilem2  25050  divcnvshft  25164  clim2prod  25169  ntrivcvg  25178  ntrivcvgfvn0  25180  ntrivcvgtail  25181  ntrivcvgmullem  25182  ntrivcvgmul  25183  zprod  25216  dfpo2  25326  predss  25387  wfrlem7  25476  frrlem7  25505  txpss3v  25632  pprodss4v  25638  relsset  25642  fixssdm  25660  fixssrn  25661  funpartss  25697  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  axcontlem10  25816  colinearex  25898  areacirc  26187  fneer  26258  neibastop1  26278  neibastop2lem  26279  filnetlem2  26298  filnetlem3  26299  caures  26356  bnd2lem  26390  ismtyres  26407  eldiophb  26705  monotuz  26894  fglmod  27039  pwssplit4  27059  dsmmbase  27069  frlmsslsp  27116  pwfi2f1o  27128  mvdco  27256  symgsssg  27276  psgnghm  27305  rabexgf  27562  stoweidlem26  27642  stoweidlem44  27660  stoweidlem50  27666  stoweidlem51  27667  stoweidlem52  27668  stoweidlem57  27673  stoweidlem59  27675  frgrawopreg1  28153  frgrawopreg2  28154  bnj21  28788  bnj1146  28868  bnj1292  28893  bnj1293  28894  bnj1145  29068  bnj1177  29081  toycom  29455  dihglblem2N  31777  lcdvbase  32076  mapdunirnN  32133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator