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

Theorem sseqtr4d 3600
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 2611 . 2 (𝜑𝐵 = 𝐶)
41, 3sseqtrd 3599 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-in 3542  df-ss 3549
This theorem is referenced by:  syl5sseqr  3612  fnfvima  6374  wfrlem17  7291  oaordi  7486  omordi  7506  omlimcl  7518  oen0  7526  domunsncan  7918  f1opwfi  8126  cantnfle  8424  cantnflt  8425  cantnflem1d  8441  r1pwss  8503  rankxplim3  8600  acndom2  8733  fodomfi2  8739  cflm  8928  cflim2  8941  isf34lem5  9056  isf34lem7  9057  isf34lem6  9058  axdc2lem  9126  ttukeylem5  9191  wunex2  9412  ccatass  13166  swrdval2  13214  swrdccatin12  13284  splfv2a  13300  revccat  13308  cshimadifsn  13368  cshimadifsn0  13369  rtrclreclem1  13588  rtrclreclem2  13589  sumrblem  14231  prodrblem  14440  dfphi2  15259  vdwlem1  15465  imasaddfnlem  15953  imasaddvallem  15954  imasvscafn  15962  imasvscaval  15963  mreexexlem4d  16072  mreexfidimd  16076  sscpwex  16240  acsmap2d  16944  gsumress  17041  subsubm  17122  frmdsssubm  17163  frmdss2  17165  subsubg  17382  cntzmhm2  17537  cntzcmnf  18013  ablcntzd  18025  gsumzsubmcl  18083  gsumconst  18099  gsumzmhm  18102  gsumzoppg  18109  subgdmdprd  18198  dprdcntz2  18202  dprd2da  18206  dmdprdsplit2lem  18209  ablfac1eu  18237  pgpfaclem1  18245  pgpfaclem2  18246  issubdrg  18570  subsubrg  18571  lmhmlsp  18812  lspsntri  18860  lspindpi  18895  lidldvgen  19018  opsrtoslem2  19248  gsumfsum  19574  mrccss  19795  frlmsslsp  19892  scmatsgrp1  20085  toponss  20482  ssntr  20610  elcls3  20635  toponmre  20645  neiptoptop  20683  neiptopnei  20684  neitr  20732  ordtbas  20744  ordtopn1  20746  ordtopn2  20747  iscnp3  20796  tgcn  20804  tgcnp  20805  ssidcn  20807  cnclsi  20824  cncls  20826  cncnp  20832  lmcld  20855  tgcmp  20952  cnconn  20973  conima  20976  clscon  20981  concompcld  20985  1stccnp  21013  kgentopon  21089  llycmpkgen2  21101  1stckgen  21105  kgencn2  21108  ptopn  21134  txcls  21155  ptpjcn  21162  ptclsg  21166  xkoccn  21170  txcnp  21171  ptcnplem  21172  txcmplem2  21193  xkoptsub  21205  xkopt  21206  xkoco2cn  21209  xkococnlem  21210  xkoinjcn  21238  imasnopn  21241  imasncld  21242  imasncls  21243  qtopkgen  21261  basqtop  21262  tgqtop  21263  qtoprest  21268  kqsat  21282  kqcldsat  21284  kqnrmlem1  21294  kqnrmlem2  21295  hmeontr  21320  reghmph  21344  nrmhmph  21345  fmfnfmlem4  21509  fmfnfm  21510  flimopn  21527  flimclslem  21536  flfnei  21543  lmflf  21557  txflf  21558  fclsopn  21566  fclsfnflim  21579  alexsublem  21596  ptcmplem3  21606  cnextcn  21619  symgtgp  21653  submtmd  21656  subgtgp  21657  clssubg  21660  clsnsg  21661  tgpconcompeqg  21663  snclseqg  21667  tsmscls  21689  trust  21781  restutop  21789  restutopopn  21790  utop3cls  21803  utopreg  21804  trcfilu  21846  blssec  21987  prdsbl  22043  blssopn  22047  metcnp  22093  cfilucfil  22111  psmetutop  22119  iccntr  22360  icccmplem2  22362  reconnlem1  22365  metnrmlem1a  22396  metnrmlem1  22397  metnrmlem2  22398  metnrmlem3  22399  cnheibor  22489  lebnumlem1  22495  lebnumlem3  22497  lebnumii  22500  clsocv  22771  iscfil2  22786  iscmet3  22813  cmetss  22834  relcmpcmet  22836  bcthlem5  22846  itg1addlem5  23186  perfdvf  23386  dvres3  23396  dvres3a  23397  dvcmul  23426  dvcmulf  23427  dvlip2  23475  lhop1lem  23493  dvcnvrelem1  23497  dvcnvrelem2  23498  dvcnvre  23499  dvcvx  23500  plyco0  23665  plyaddlem1  23686  plymullem1  23687  aalioulem3  23806  ulmdvlem1  23871  axcontlem10  25567  eengtrkg  25579  eupares  26264  hsupunss  27388  pjpjpre  27464  ssmd2  28357  superpos  28399  atexch  28426  curry2ima  28671  madjusmdetlem2  29024  ordtconlem1  29100  measiuns  29409  imambfm  29453  cnmbfm  29454  dya2iocnrect  29472  omsfval  29485  omssubaddlem  29490  omssubadd  29491  totprobd  29617  fzssfzo  29742  signstfvn  29774  bnj999  30083  bnj1408  30160  bnj1442  30173  bnj1450  30174  bnj1501  30191  cvmsss2  30312  cvmliftmolem1  30319  cvmliftlem3  30325  cvmlift2lem9  30349  cvmlift2lem11  30351  cvmlift3lem6  30362  cvmlift3lem7  30363  ssmclslem  30518  mclsax  30522  mclsppslem  30536  mclspps  30537  dfrdg2  30747  trpredtr  30776  neiin  31299  neibastop2  31328  filnetlem4  31348  lindsdom  32372  poimirlem11  32389  poimirlem12  32390  itg2addnclem2  32431  cnres2  32531  sstotbnd2  32542  sstotbnd  32543  prdstotbnd  32562  heibor1lem  32577  igenval2  32834  lshpnelb  33088  lcvexchlem4  33141  lsatexch  33147  l1cvat  33159  lkrscss  33202  lkrss  33272  lkreqN  33274  paddunN  34030  osumcllem2N  34060  pmapojoinN  34071  pl42lem2N  34083  dibglbN  35272  diblss  35276  dicvaddcl  35296  dicvscacl  35297  diclss  35299  cdlemn5pre  35306  dihord5apre  35368  dihglblem3N  35401  dihglb2  35448  dochsat  35489  dochshpncl  35490  djhspss  35512  dihsumssj  35514  mapdlsm  35770  hdmaprnlem3eN  35967  hdmaplkr  36022  fnwe2lem2  36438  lnmlsslnm  36468  lmhmfgima  36471  hbtlem6  36517  trrelsuperreldg  36778  iunrelexpuztr  36829  clsk1indlem2  37159  funfvima2d  37290  dvsconst  37350  dvsinax  38601  dvbdfbdioolem1  38618  itgsinexplem1  38645  itgperiod  38673  stoweidlem39  38732  dirkeritg  38795  fourierdlem48  38847  fourierdlem49  38848  fourierdlem70  38869  fourierdlem71  38870  fourierdlem81  38880  issalgend  39032  pfxccatin12  40089  uhgrstrrepelem  40301  nbupgruvtxres  40632  1wlkp1lem7  40886  11wlkdlem4  41305  subsubmgm  41585  rmsuppss  41943
  Copyright terms: Public domain W3C validator