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

Theorem eqsstr3d 3328
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 2394 . 2  |-  ( ph  ->  A  =  B )
3 eqsstr3d.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3eqsstrd 3327 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3265
This theorem is referenced by:  ssxpb  5245  suppssof1  6287  oaword1  6733  omword2  6755  oeeui  6783  nnaword1  6810  cantnfle  7561  cantnflem1d  7579  r1val1  7647  rankr1id  7723  rankxplim3  7740  ackbij2  8058  ttukeylem7  8330  gruima  8612  rlimi  12236  rlimi2  12237  lo1bdd  12243  o1bdd  12254  rlimuni  12273  rlimcld2  12301  o1co  12309  rlimcn1  12311  rlimcn2  12313  o1add2  12346  o1mul2  12347  o1sub2  12348  lo1add  12349  lo1mul  12350  o1dif  12352  rlimneg  12369  rlimsqzlem  12371  lo1le  12374  rlimno1  12376  ramub1lem1  13323  imasaddfnlem  13682  imasvscafn  13691  mrcidb  13769  mrieqv2d  13793  mreexexlem4d  13801  funcres  14022  funcsetcres2  14177  acsfiindd  14532  tsrdir  14612  resmhm2  14689  sylow2a  15182  sylow3lem6  15195  dprdspan  15514  dprd2dlem2  15527  dprd2dlem1  15528  dprd2da  15529  dmdprdsplit2lem  15532  dprdsplit  15535  dpjcntz  15539  ablfac1eu  15560  rngidss  15619  subrg1  15807  subrgdvds  15811  subrguss  15812  subrginv  15813  islss3  15964  lspsnneg  16011  lspextmo  16061  lspsnvs  16115  lsmcv  16142  islbs3  16156  drngdomn  16292  psrbaglesupp  16362  psrbas  16372  psrlidm  16396  psrridm  16397  resspsrbas  16407  resspsradd  16408  resspsrmul  16409  epttop  16998  neitr  17168  ordtbas  17180  ordtrest2  17192  pnfnei  17208  mnfnei  17209  ordtrestixx  17210  dnsconst  17366  cmpcld  17389  txindis  17589  txtube  17595  xkohaus  17608  xkopt  17610  xkococnlem  17614  xkoinjcn  17642  qtopval2  17651  ssufl  17873  ufldom  17917  cnextcn  18021  tmdgsum2  18049  clssubg  18061  clsnsg  18062  ustund  18174  ustneism  18176  trust  18182  fmucnd  18245  imasdsf1olem  18313  setsmstopn  18400  metequiv2  18432  metust  18480  restmetu  18491  tngtopn  18564  xlebnum  18863  pi1xfrcnv  18955  limcdif  19632  limccnp  19647  limccnp2  19648  limcco  19649  dvn2bss  19685  cpnord  19690  dvcmulf  19700  dvmptres2  19717  dvmptcmul  19719  dvmptntr  19726  dvcnvrelem2  19771  dvcnvre  19772  evlseu  19806  taylthlem1  20158  taylthlem2  20159  ulmdvlem3  20187  psercnlem2  20209  rlimcxp  20681  o1cxp  20682  nbgrassovt  21315  sspg  22077  ssps  22079  sspn  22085  mdslj1i  23672  mdslj2i  23673  sh1dle  23704  shatomistici  23714  sumdmdii  23768  cnvordtrestixx  24117  dya2iocucvr  24430  cvmscld  24741  nofulllem3  25384  fvline2  25796  cldregopn  26027  sstotbnd2  26176  totbndbnd  26191  heibor1  26212  heiborlem8  26220  dnnumch2  26813  f1lindf  26963  f1omvdco2  27062  bnj142  28433  bnj1241  28519  bnj906  28641  lsmsat  29125  lssats  29129  lkrpssN  29280  dia2dimlem5  31185  cdlemn2a  31313  dihglblem6  31457  dochocsp  31496  dochdmj1  31507  dochsatshpb  31569  lcfl9a  31622  lclkrlem2r  31641  lclkrlem2s  31642  lclkrlem2v  31645  lcfrlem6  31664  lcfrlem25  31684  lcfrlem35  31694  mapdval2N  31747  mapdin  31779  baerlem5alem2  31828  baerlem5blem2  31829
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
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 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator