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

Theorem eqsstr3d 3538
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
eqsstr3d.1
eqsstr3d.2
Assertion
Ref Expression
eqsstr3d

Proof of Theorem eqsstr3d
StepHypRef Expression
1 eqsstr3d.1 . . 3
21eqcomd 2465 . 2
3 eqsstr3d.2 . 2
42, 3eqsstrd 3537 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  ssxpb  5446  fnsnb  6090  suppssof1OLD  6559  suppssof1  6952  oaword1  7220  omword2  7242  oeeui  7270  nnaword1  7297  cantnfle  8111  cantnflem1d  8128  cantnfleOLD  8141  cantnflem1dOLD  8151  r1val1  8225  rankr1id  8301  rankxplim3  8320  ackbij2  8644  ttukeylem7  8916  gruima  9201  rlimi  13336  rlimi2  13337  lo1bdd  13343  o1bdd  13354  rlimuni  13373  rlimcld2  13401  o1co  13409  rlimcn1  13411  rlimcn2  13413  o1add2  13446  o1mul2  13447  o1sub2  13448  lo1add  13449  lo1mul  13450  o1dif  13452  rlimneg  13469  rlimsqzlem  13471  lo1le  13474  rlimno1  13476  ramub1lem1  14544  imasaddfnlem  14925  imasvscafn  14934  mrcidb  15012  mrieqv2d  15036  mreexexlem4d  15044  funcres  15265  funcsetcres2  15420  acsfiindd  15807  tsrdir  15868  resmhm2  15991  f1omvdco2  16473  sylow2a  16639  sylow3lem6  16652  dprdspan  17074  dprd2dlem2  17089  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2lem  17094  dprdsplit  17097  dpjcntz  17101  ablfac1eu  17124  ringidss  17225  subrg1  17439  subrgdvds  17443  subrguss  17444  subrginv  17445  islss3  17605  lspsnneg  17652  lspextmo  17702  lspsnvs  17760  lsmcv  17787  islbs3  17801  drngdomn  17952  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbasOLD  18031  psrlidmOLD  18057  psrridmOLD  18059  resspsrbas  18070  resspsradd  18071  resspsrmul  18072  evlseu  18185  f1lindf  18857  epttop  19510  neitr  19681  ordtbas  19693  ordtrest2  19705  pnfnei  19721  mnfnei  19722  ordtrestixx  19723  dnsconst  19879  cmpcld  19902  txindis  20135  txtube  20141  xkohaus  20154  xkopt  20156  xkococnlem  20160  xkoinjcn  20188  qtopval2  20197  ssufl  20419  ufldom  20463  cnextcn  20567  tmdgsum2  20595  clssubg  20607  clsnsg  20608  ustund  20724  ustneism  20726  trust  20732  fmucnd  20795  imasdsf1olem  20876  setsmstopn  20981  metequiv2  21013  metustOLD  21070  metust  21071  restmetu  21090  tngtopn  21164  xlebnum  21465  pi1xfrcnv  21557  limcdif  22280  limccnp  22295  limccnp2  22296  limcco  22297  dvn2bss  22333  cpnord  22338  dvcmulf  22348  dvmptres2  22365  dvmptcmul  22367  dvmptntr  22374  dvcnvrelem2  22419  dvcnvre  22420  taylthlem1  22768  taylthlem2  22769  ulmdvlem3  22797  psercnlem2  22819  rlimcxp  23303  o1cxp  23304  nbgrassovt  24435  sspg  25641  ssps  25643  sspn  25649  mdslj1i  27238  mdslj2i  27239  sh1dle  27270  shatomistici  27280  sumdmdii  27334  resf1o  27553  submarchi  27730  txomap  27837  cnvordtrestixx  27895  dya2iocucvr  28255  cvmscld  28718  nofulllem3  29464  fvline2  29796  cldregopn  30149  sstotbnd2  30270  totbndbnd  30285  heibor1  30306  heiborlem8  30314  dnnumch2  30991  mullimc  31622  islptre  31625  mullimcf  31629  limcmptdm  31641  dvresntr  31713  itgperiod  31780  fourierdlem89  31978  fourierdlem91  31980  resmgmhm2  32487  bnj142OLD  33781  bnj1241  33866  bnj906  33988  lsmsat  34733  lssats  34737  lkrpssN  34888  dia2dimlem5  36795  cdlemn2a  36923  dihglblem6  37067  dochocsp  37106  dochdmj1  37117  dochsatshpb  37179  lcfl9a  37232  lclkrlem2r  37251  lclkrlem2s  37252  lclkrlem2v  37255  lcfrlem6  37274  lcfrlem25  37294  lcfrlem35  37304  mapdval2N  37357  mapdin  37389  baerlem5alem2  37438  baerlem5blem2  37439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator