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

Theorem eqsstr3d 3385
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 2443 . 2  |-  ( ph  ->  A  =  B )
3 eqsstr3d.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3eqsstrd 3384 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3322
This theorem is referenced by:  ssxpb  5306  suppssof1  6349  oaword1  6798  omword2  6820  oeeui  6848  nnaword1  6875  cantnfle  7629  cantnflem1d  7647  r1val1  7715  rankr1id  7791  rankxplim3  7810  ackbij2  8128  ttukeylem7  8400  gruima  8682  rlimi  12312  rlimi2  12313  lo1bdd  12319  o1bdd  12330  rlimuni  12349  rlimcld2  12377  o1co  12385  rlimcn1  12387  rlimcn2  12389  o1add2  12422  o1mul2  12423  o1sub2  12424  lo1add  12425  lo1mul  12426  o1dif  12428  rlimneg  12445  rlimsqzlem  12447  lo1le  12450  rlimno1  12452  ramub1lem1  13399  imasaddfnlem  13758  imasvscafn  13767  mrcidb  13845  mrieqv2d  13869  mreexexlem4d  13877  funcres  14098  funcsetcres2  14253  acsfiindd  14608  tsrdir  14688  resmhm2  14765  sylow2a  15258  sylow3lem6  15271  dprdspan  15590  dprd2dlem2  15603  dprd2dlem1  15604  dprd2da  15605  dmdprdsplit2lem  15608  dprdsplit  15611  dpjcntz  15615  ablfac1eu  15636  rngidss  15695  subrg1  15883  subrgdvds  15887  subrguss  15888  subrginv  15889  islss3  16040  lspsnneg  16087  lspextmo  16137  lspsnvs  16191  lsmcv  16218  islbs3  16232  drngdomn  16368  psrbaglesupp  16438  psrbas  16448  psrlidm  16472  psrridm  16473  resspsrbas  16483  resspsradd  16484  resspsrmul  16485  epttop  17078  neitr  17249  ordtbas  17261  ordtrest2  17273  pnfnei  17289  mnfnei  17290  ordtrestixx  17291  dnsconst  17447  cmpcld  17470  txindis  17671  txtube  17677  xkohaus  17690  xkopt  17692  xkococnlem  17696  xkoinjcn  17724  qtopval2  17733  ssufl  17955  ufldom  17999  cnextcn  18103  tmdgsum2  18131  clssubg  18143  clsnsg  18144  ustund  18256  ustneism  18258  trust  18264  fmucnd  18327  imasdsf1olem  18408  setsmstopn  18513  metequiv2  18545  metustOLD  18602  metust  18603  restmetu  18622  tngtopn  18696  xlebnum  18995  pi1xfrcnv  19087  limcdif  19768  limccnp  19783  limccnp2  19784  limcco  19785  dvn2bss  19821  cpnord  19826  dvcmulf  19836  dvmptres2  19853  dvmptcmul  19855  dvmptntr  19862  dvcnvrelem2  19907  dvcnvre  19908  evlseu  19942  taylthlem1  20294  taylthlem2  20295  ulmdvlem3  20323  psercnlem2  20345  rlimcxp  20817  o1cxp  20818  nbgrassovt  21452  sspg  22232  ssps  22234  sspn  22240  mdslj1i  23827  mdslj2i  23828  sh1dle  23859  shatomistici  23869  sumdmdii  23923  cnvordtrestixx  24316  dya2iocucvr  24639  cvmscld  24965  nofulllem3  25664  fvline2  26085  cldregopn  26348  sstotbnd2  26497  totbndbnd  26512  heibor1  26533  heiborlem8  26541  dnnumch2  27134  f1lindf  27283  f1omvdco2  27382  bnj142  29167  bnj1241  29253  bnj906  29375  lsmsat  29880  lssats  29884  lkrpssN  30035  dia2dimlem5  31940  cdlemn2a  32068  dihglblem6  32212  dochocsp  32251  dochdmj1  32262  dochsatshpb  32324  lcfl9a  32377  lclkrlem2r  32396  lclkrlem2s  32397  lclkrlem2v  32400  lcfrlem6  32419  lcfrlem25  32439  lcfrlem35  32449  mapdval2N  32502  mapdin  32534  baerlem5alem2  32583  baerlem5blem2  32584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator