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

Theorem eqsstr3d 3213
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 2288 . 2  |-  ( ph  ->  A  =  B )
3 eqsstr3d.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3eqsstrd 3212 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  ssxpb  5110  ffvresb  5690  suppssof1  6119  oaword1  6550  omword2  6572  oeeui  6600  nnaword1  6627  cantnfle  7372  cantnflem1d  7390  r1val1  7458  rankr1id  7534  rankxpl  7547  rankxplim3  7551  ackbij2  7869  ttukeylem7  8142  winafp  8319  wunex2  8360  gruima  8424  iooval2  10689  rlimi  11987  rlimi2  11988  lo1bdd  11994  o1bdd  12005  rlimuni  12024  rlimcld2  12052  o1co  12060  rlimcn1  12062  rlimcn2  12064  o1add2  12097  o1mul2  12098  o1sub2  12099  lo1add  12100  lo1mul  12101  o1dif  12103  rlimneg  12120  rlimsqzlem  12122  lo1le  12125  rlimno1  12127  fsumtscopo  12260  ramub1lem1  13073  structcnvcnv  13159  ressbasss  13200  imasaddfnlem  13430  imasvscafn  13439  mrcidb  13517  mrieqv2d  13541  mreexexlem4d  13549  funcres  13770  funcsetcres2  13925  acsfiindd  14280  tsrdir  14360  resmhm2  14437  sylow2a  14930  sylow3lem6  14943  dprdspan  15262  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  dprdsplit  15283  dpjcntz  15287  ablfac1eu  15308  rngidss  15367  subrg1  15555  subrgdvds  15559  subrguss  15560  subrginv  15561  islss3  15716  lspsnneg  15763  lspextmo  15813  lspsnvs  15867  lsmcv  15894  islbs3  15908  drngdomn  16044  psrbaglesupp  16114  psrbas  16124  psrlidm  16148  psrridm  16149  resspsrbas  16159  resspsradd  16160  resspsrmul  16161  opsrtoslem2  16226  epttop  16746  ordtbas  16922  ordtrest2  16934  pnfnei  16950  mnfnei  16951  ordtrestixx  16952  dnsconst  17106  cmpcld  17129  txindis  17328  txtube  17334  xkohaus  17347  xkopt  17349  xkococnlem  17353  xkoinjcn  17381  qtopval2  17387  ssufl  17613  fmss  17641  ufldom  17657  tmdgsum2  17779  clssubg  17791  clsnsg  17792  imasdsf1olem  17937  setsmstopn  18024  metequiv2  18056  tngtopn  18166  xlebnum  18463  pi1xfrcnv  18555  limcdif  19226  limccnp  19241  limccnp2  19242  limcco  19243  dvn2bss  19279  cpnord  19284  dvaddf  19291  dvmulf  19292  dvcmulf  19294  dvcof  19297  dvmptres3  19305  dvmptres2  19311  dvmptcmul  19313  dvmptcj  19317  dvmptntr  19320  dvcnvlem  19323  dvcnv  19324  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  evlseu  19400  plyrem  19685  taylthlem1  19752  taylthlem2  19753  ulmss  19774  ulmdvlem1  19777  ulmdvlem3  19779  ulmdv  19780  psercnlem2  19800  rlimcxp  20268  o1cxp  20269  isppw  20352  sspg  21304  ssps  21306  sspn  21312  mdslj1i  22899  mdslj2i  22900  sh1dle  22931  shatomistici  22941  sumdmdii  22995  cvmscld  23215  nofulllem3  23769  fvline2  24180  altretop  25012  cldregopn  25661  sstotbnd2  25910  totbndbnd  25925  heibor1  25946  heiborlem8  25954  dnnumch2  26554  dsmmsubg  26621  f1lindf  26704  hbtlem6  26745  f1omvdco2  26803  symgsssg  26820  bnj142  28127  bnj1241  28213  bnj906  28335  lsmsat  28571  lssats  28575  lkrpssN  28726  dia2dimlem5  30631  cdlemn2a  30759  dihglblem6  30903  dochocsp  30942  dochdmj1  30953  dochsatshpb  31015  lcfl9a  31068  lclkrlem2r  31087  lclkrlem2s  31088  lclkrlem2v  31091  lcfrlem6  31110  lcfrlem25  31130  lcfrlem35  31140  mapdval2N  31193  mapdin  31225  baerlem5alem2  31274  baerlem5blem2  31275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator