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

Theorem eqsstr3d 3226
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstr3d.1  |-  ( ph  ->  B  =  A )
eqsstr3d.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
eqsstr3d  |-  ( ph  ->  A  C_  C )

Proof of Theorem eqsstr3d
StepHypRef Expression
1 eqsstr3d.1 . . 3  |-  ( ph  ->  B  =  A )
21eqcomd 2301 . 2  |-  ( ph  ->  A  =  B )
3 eqsstr3d.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3eqsstrd 3225 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  ssxpb  5126  ffvresb  5706  suppssof1  6135  oaword1  6566  omword2  6588  oeeui  6616  nnaword1  6643  cantnfle  7388  cantnflem1d  7406  r1val1  7474  rankr1id  7550  rankxpl  7563  rankxplim3  7567  ackbij2  7885  ttukeylem7  8158  winafp  8335  wunex2  8376  gruima  8440  iooval2  10705  rlimi  12003  rlimi2  12004  lo1bdd  12010  o1bdd  12021  rlimuni  12040  rlimcld2  12068  o1co  12076  rlimcn1  12078  rlimcn2  12080  o1add2  12113  o1mul2  12114  o1sub2  12115  lo1add  12116  lo1mul  12117  o1dif  12119  rlimneg  12136  rlimsqzlem  12138  lo1le  12141  rlimno1  12143  fsumtscopo  12276  ramub1lem1  13089  structcnvcnv  13175  ressbasss  13216  imasaddfnlem  13446  imasvscafn  13455  mrcidb  13533  mrieqv2d  13557  mreexexlem4d  13565  funcres  13786  funcsetcres2  13941  acsfiindd  14296  tsrdir  14376  resmhm2  14453  sylow2a  14946  sylow3lem6  14959  dprdspan  15278  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  dmdprdsplit2lem  15296  dprdsplit  15299  dpjcntz  15303  ablfac1eu  15324  rngidss  15383  subrg1  15571  subrgdvds  15575  subrguss  15576  subrginv  15577  islss3  15732  lspsnneg  15779  lspextmo  15829  lspsnvs  15883  lsmcv  15910  islbs3  15924  drngdomn  16060  psrbaglesupp  16130  psrbas  16140  psrlidm  16164  psrridm  16165  resspsrbas  16175  resspsradd  16176  resspsrmul  16177  opsrtoslem2  16242  epttop  16762  ordtbas  16938  ordtrest2  16950  pnfnei  16966  mnfnei  16967  ordtrestixx  16968  dnsconst  17122  cmpcld  17145  txindis  17344  txtube  17350  xkohaus  17363  xkopt  17365  xkococnlem  17369  xkoinjcn  17397  qtopval2  17403  ssufl  17629  fmss  17657  ufldom  17673  tmdgsum2  17795  clssubg  17807  clsnsg  17808  imasdsf1olem  17953  setsmstopn  18040  metequiv2  18072  tngtopn  18182  xlebnum  18479  pi1xfrcnv  18571  limcdif  19242  limccnp  19257  limccnp2  19258  limcco  19259  dvn2bss  19295  cpnord  19300  dvaddf  19307  dvmulf  19308  dvcmulf  19310  dvcof  19313  dvmptres3  19321  dvmptres2  19327  dvmptcmul  19329  dvmptcj  19333  dvmptntr  19336  dvcnvlem  19339  dvcnv  19340  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  evlseu  19416  plyrem  19701  taylthlem1  19768  taylthlem2  19769  ulmss  19790  ulmdvlem1  19793  ulmdvlem3  19795  ulmdv  19796  psercnlem2  19816  rlimcxp  20284  o1cxp  20285  isppw  20368  sspg  21320  ssps  21322  sspn  21328  mdslj1i  22915  mdslj2i  22916  sh1dle  22947  shatomistici  22957  sumdmdii  23011  cnvordtrestixx  23312  cvmscld  23819  nofulllem3  24429  fvline2  24841  altretop  25703  cldregopn  26352  sstotbnd2  26601  totbndbnd  26616  heibor1  26637  heiborlem8  26645  dnnumch2  27245  dsmmsubg  27312  f1lindf  27395  hbtlem6  27436  f1omvdco2  27494  symgsssg  27511  nbgrassovt  28284  bnj142  29070  bnj1241  29156  bnj906  29278  lsmsat  29820  lssats  29824  lkrpssN  29975  dia2dimlem5  31880  cdlemn2a  32008  dihglblem6  32152  dochocsp  32191  dochdmj1  32202  dochsatshpb  32264  lcfl9a  32317  lclkrlem2r  32336  lclkrlem2s  32337  lclkrlem2v  32340  lcfrlem6  32359  lcfrlem25  32379  lcfrlem35  32389  mapdval2N  32442  mapdin  32474  baerlem5alem2  32523  baerlem5blem2  32524
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator