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

Theorem eqsstr3d 3375
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 2440 . 2  |-  ( ph  ->  A  =  B )
3 eqsstr3d.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3eqsstrd 3374 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  ssxpb  5295  suppssof1  6338  oaword1  6787  omword2  6809  oeeui  6837  nnaword1  6864  cantnfle  7618  cantnflem1d  7636  r1val1  7704  rankr1id  7780  rankxplim3  7797  ackbij2  8115  ttukeylem7  8387  gruima  8669  rlimi  12299  rlimi2  12300  lo1bdd  12306  o1bdd  12317  rlimuni  12336  rlimcld2  12364  o1co  12372  rlimcn1  12374  rlimcn2  12376  o1add2  12409  o1mul2  12410  o1sub2  12411  lo1add  12412  lo1mul  12413  o1dif  12415  rlimneg  12432  rlimsqzlem  12434  lo1le  12437  rlimno1  12439  ramub1lem1  13386  imasaddfnlem  13745  imasvscafn  13754  mrcidb  13832  mrieqv2d  13856  mreexexlem4d  13864  funcres  14085  funcsetcres2  14240  acsfiindd  14595  tsrdir  14675  resmhm2  14752  sylow2a  15245  sylow3lem6  15258  dprdspan  15577  dprd2dlem2  15590  dprd2dlem1  15591  dprd2da  15592  dmdprdsplit2lem  15595  dprdsplit  15598  dpjcntz  15602  ablfac1eu  15623  rngidss  15682  subrg1  15870  subrgdvds  15874  subrguss  15875  subrginv  15876  islss3  16027  lspsnneg  16074  lspextmo  16124  lspsnvs  16178  lsmcv  16205  islbs3  16219  drngdomn  16355  psrbaglesupp  16425  psrbas  16435  psrlidm  16459  psrridm  16460  resspsrbas  16470  resspsradd  16471  resspsrmul  16472  epttop  17065  neitr  17236  ordtbas  17248  ordtrest2  17260  pnfnei  17276  mnfnei  17277  ordtrestixx  17278  dnsconst  17434  cmpcld  17457  txindis  17658  txtube  17664  xkohaus  17677  xkopt  17679  xkococnlem  17683  xkoinjcn  17711  qtopval2  17720  ssufl  17942  ufldom  17986  cnextcn  18090  tmdgsum2  18118  clssubg  18130  clsnsg  18131  ustund  18243  ustneism  18245  trust  18251  fmucnd  18314  imasdsf1olem  18395  setsmstopn  18500  metequiv2  18532  metustOLD  18589  metust  18590  restmetu  18609  tngtopn  18683  xlebnum  18982  pi1xfrcnv  19074  limcdif  19755  limccnp  19770  limccnp2  19771  limcco  19772  dvn2bss  19808  cpnord  19813  dvcmulf  19823  dvmptres2  19840  dvmptcmul  19842  dvmptntr  19849  dvcnvrelem2  19894  dvcnvre  19895  evlseu  19929  taylthlem1  20281  taylthlem2  20282  ulmdvlem3  20310  psercnlem2  20332  rlimcxp  20804  o1cxp  20805  nbgrassovt  21439  sspg  22219  ssps  22221  sspn  22227  mdslj1i  23814  mdslj2i  23815  sh1dle  23846  shatomistici  23856  sumdmdii  23910  cnvordtrestixx  24303  dya2iocucvr  24626  cvmscld  24952  nofulllem3  25651  fvline2  26072  cldregopn  26325  sstotbnd2  26474  totbndbnd  26489  heibor1  26510  heiborlem8  26518  dnnumch2  27111  f1lindf  27260  f1omvdco2  27359  bnj142  29030  bnj1241  29116  bnj906  29238  lsmsat  29743  lssats  29747  lkrpssN  29898  dia2dimlem5  31803  cdlemn2a  31931  dihglblem6  32075  dochocsp  32114  dochdmj1  32125  dochsatshpb  32187  lcfl9a  32240  lclkrlem2r  32259  lclkrlem2s  32260  lclkrlem2v  32263  lcfrlem6  32282  lcfrlem25  32302  lcfrlem35  32312  mapdval2N  32365  mapdin  32397  baerlem5alem2  32446  baerlem5blem2  32447
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator