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

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

Proof of Theorem sseqtr4d
StepHypRef Expression
1 sseqtr4d.1 . 2
2 sseqtr4d.2 . . 3
32eqcomd 2465 . 2
41, 3sseqtrd 3539 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  syl5sseqr  3552  reusv6OLD  4663  fnfvima  6150  oaordi  7214  omordi  7234  omlimcl  7246  oen0  7254  domunsncan  7637  f1opwfi  7844  cantnfle  8111  cantnflt  8112  cantnflem1d  8128  cantnfleOLD  8141  cantnfltOLD  8142  cantnflem1dOLD  8151  r1pwss  8223  rankxplim3  8320  acndom2  8456  fodomfi2  8462  cflm  8651  cflim2  8664  isf34lem5  8779  isf34lem7  8780  isf34lem6  8781  axdc2lem  8849  ttukeylem5  8914  wunex2  9137  ccatass  12605  swrdval2  12647  swrdccatin12  12716  splfv2a  12732  revccat  12740  sumrblem  13533  prodrblem  13736  dfphi2  14304  vdwlem1  14499  imasaddfnlem  14925  imasaddvallem  14926  imasvscafn  14934  imasvscaval  14935  mreexexlem4d  15044  mreexfidimd  15047  sscpwex  15184  acsmap2d  15809  gsumress  15903  subsubm  15988  frmdsssubm  16029  frmdss2  16031  subsubg  16224  cntzmhm2  16377  cntzcmnf  16851  ablcntzd  16863  gsumzsubmcl  16928  gsumzsubmclOLD  16929  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  subgdmdprd  17081  dprdcntz2  17086  dprd2da  17091  dmdprdsplit2lem  17094  ablfac1eu  17124  pgpfaclem1  17132  pgpfaclem2  17133  issubdrg  17454  subsubrg  17455  lmhmlsp  17695  lspsntri  17743  lspindpi  17778  lidldvgen  17903  opsrtoslem2  18149  gsumfsum  18484  mrccss  18725  frlmsslsp  18829  frlmsslspOLD  18830  scmatsgrp1  19024  toponss  19430  ssntr  19559  elcls3  19584  toponmre  19594  neiptoptop  19632  neiptopnei  19633  neitr  19681  ordtbas  19693  ordtopn1  19695  ordtopn2  19696  iscnp3  19745  tgcn  19753  tgcnp  19754  ssidcn  19756  cnclsi  19773  cncls  19775  cncnp  19781  lmcld  19804  tgcmp  19901  cnconn  19923  conima  19926  clscon  19931  concompcld  19935  1stccnp  19963  kgentopon  20039  llycmpkgen2  20051  1stckgen  20055  kgencn2  20058  ptopn  20084  txcls  20105  ptpjcn  20112  ptclsg  20116  xkoccn  20120  txcnp  20121  ptcnplem  20122  txcmplem2  20143  xkoptsub  20155  xkopt  20156  xkoco2cn  20159  xkococnlem  20160  xkoinjcn  20188  imasnopn  20191  imasncld  20192  imasncls  20193  qtopkgen  20211  basqtop  20212  tgqtop  20213  qtoprest  20218  kqsat  20232  kqcldsat  20234  kqnrmlem1  20244  kqnrmlem2  20245  hmeontr  20270  reghmph  20294  nrmhmph  20295  fmfnfmlem4  20458  fmfnfm  20459  flimopn  20476  flimclslem  20485  flfnei  20492  lmflf  20506  txflf  20507  fclsopn  20515  fclsfnflim  20528  alexsublem  20544  ptcmplem3  20554  cnextcn  20567  symgtgp  20600  submtmd  20603  subgtgp  20604  clssubg  20607  clsnsg  20608  tgpconcompeqg  20610  snclseqg  20614  tsmscls  20636  trust  20732  restutop  20740  restutopopn  20741  utop3cls  20754  utopreg  20755  trcfilu  20797  blssec  20938  prdsbl  20994  blssopn  20998  metcnp  21044  cfilucfilOLD  21072  cfilucfil  21073  metutopOLD  21085  psmetutop  21086  iccntr  21326  icccmplem2  21328  reconnlem1  21331  metnrmlem1a  21362  metnrmlem1  21363  metnrmlem2  21364  metnrmlem3  21365  cnheibor  21455  lebnumlem1  21461  lebnumlem3  21463  lebnumii  21466  clsocv  21690  iscfil2  21705  iscmet3  21732  cmetss  21753  relcmpcmet  21755  bcthlem5  21767  itg1addlem5  22107  perfdvf  22307  dvres3  22317  dvres3a  22318  dvcmul  22347  dvcmulf  22348  dvlip2  22396  lhop1lem  22414  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvcvx  22421  plyco0  22589  plyaddlem1  22610  plymullem1  22611  aalioulem3  22730  ulmdvlem1  22795  axcontlem10  24276  eengtrkg  24288  eupares  24975  ghsubgolemOLD  25372  hsupunss  26261  pjpjpre  26337  ssmd2  27231  superpos  27273  atexch  27300  curry2ima  27526  ordtconlem1  27906  measiuns  28188  imambfm  28233  cnmbfm  28234  dya2iocnrect  28252  totprobd  28365  fzssfzo  28490  signstfvn  28526  cvmsss2  28719  cvmliftmolem1  28726  cvmliftlem3  28732  cvmlift2lem9  28756  cvmlift2lem11  28758  cvmlift3lem6  28769  cvmlift3lem7  28770  ssmclslem  28925  mclsax  28929  mclsppslem  28943  mclspps  28944  rtrclreclem.refl  29067  rtrclreclem.subset  29068  dfrdg2  29228  trpredtr  29313  itg2addnclem2  30067  neiin  30150  neibastop2  30179  filnetlem4  30199  cnres2  30259  sstotbnd2  30270  sstotbnd  30271  prdstotbnd  30290  heibor1lem  30305  igenval2  30463  fnwe2lem2  30997  lnmlsslnm  31027  lmhmfgima  31030  hbtlem6  31078  dvsconst  31235  dvsinax  31708  dvbdfbdioolem1  31725  itgsinexplem1  31752  itgperiod  31780  stoweidlem39  31821  dirkeritg  31884  fourierdlem48  31937  fourierdlem49  31938  fourierdlem70  31959  fourierdlem71  31960  fourierdlem81  31970  subsubmgm  32485  rmsuppss  32963  bnj999  34015  bnj1408  34092  bnj1442  34105  bnj1450  34106  bnj1501  34123  lshpnelb  34709  lcvexchlem4  34762  lsatexch  34768  l1cvat  34780  lkrscss  34823  lkrss  34893  lkreqN  34895  paddunN  35651  osumcllem2N  35681  pmapojoinN  35692  pl42lem2N  35704  dibglbN  36893  diblss  36897  dicvaddcl  36917  dicvscacl  36918  diclss  36920  cdlemn5pre  36927  dihord5apre  36989  dihglblem3N  37022  dihglb2  37069  dochsat  37110  dochshpncl  37111  djhspss  37133  dihsumssj  37135  mapdlsm  37391  hdmaprnlem3eN  37588  hdmaplkr  37643  trrelsuperreldg  37783  funfvima2d  37986
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