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

Theorem sseqtr4d 3501
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtr4d.1  |-  ( ph  ->  A  C_  B )
sseqtr4d.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
sseqtr4d  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtr4d
StepHypRef Expression
1 sseqtr4d.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtr4d.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2430 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3500 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  syl5sseqr  3513  fnfvima  6158  wfrlem17  7063  oaordi  7258  omordi  7278  omlimcl  7290  oen0  7298  domunsncan  7681  f1opwfi  7887  cantnfle  8184  cantnflt  8185  cantnflem1d  8201  r1pwss  8263  rankxplim3  8360  acndom2  8492  fodomfi2  8498  cflm  8687  cflim2  8700  isf34lem5  8815  isf34lem7  8816  isf34lem6  8817  axdc2lem  8885  ttukeylem5  8950  wunex2  9170  ccatass  12736  swrdval2  12778  swrdccatin12  12849  splfv2a  12865  revccat  12873  rtrclreclem1  13121  rtrclreclem2  13122  sumrblem  13776  prodrblem  13982  dfphi2  14721  vdwlem1  14930  imasaddfnlem  15433  imasaddvallem  15434  imasvscafn  15442  imasvscaval  15443  mreexexlem4d  15552  mreexfidimd  15555  sscpwex  15719  acsmap2d  16424  gsumress  16518  subsubm  16603  frmdsssubm  16644  frmdss2  16646  subsubg  16839  cntzmhm2  16992  cntzcmnf  17482  ablcntzd  17494  gsumzsubmcl  17550  gsumconst  17566  gsumzmhm  17569  gsumzoppg  17576  subgdmdprd  17666  dprdcntz2  17670  dprd2da  17674  dmdprdsplit2lem  17677  ablfac1eu  17705  pgpfaclem1  17713  pgpfaclem2  17714  issubdrg  18032  subsubrg  18033  lmhmlsp  18271  lspsntri  18319  lspindpi  18354  lidldvgen  18478  opsrtoslem2  18707  gsumfsum  19033  mrccss  19255  frlmsslsp  19352  scmatsgrp1  19545  toponss  19942  ssntr  20071  elcls3  20097  toponmre  20107  neiptoptop  20145  neiptopnei  20146  neitr  20194  ordtbas  20206  ordtopn1  20208  ordtopn2  20209  iscnp3  20258  tgcn  20266  tgcnp  20267  ssidcn  20269  cnclsi  20286  cncls  20288  cncnp  20294  lmcld  20317  tgcmp  20414  cnconn  20435  conima  20438  clscon  20443  concompcld  20447  1stccnp  20475  kgentopon  20551  llycmpkgen2  20563  1stckgen  20567  kgencn2  20570  ptopn  20596  txcls  20617  ptpjcn  20624  ptclsg  20628  xkoccn  20632  txcnp  20633  ptcnplem  20634  txcmplem2  20655  xkoptsub  20667  xkopt  20668  xkoco2cn  20671  xkococnlem  20672  xkoinjcn  20700  imasnopn  20703  imasncld  20704  imasncls  20705  qtopkgen  20723  basqtop  20724  tgqtop  20725  qtoprest  20730  kqsat  20744  kqcldsat  20746  kqnrmlem1  20756  kqnrmlem2  20757  hmeontr  20782  reghmph  20806  nrmhmph  20807  fmfnfmlem4  20970  fmfnfm  20971  flimopn  20988  flimclslem  20997  flfnei  21004  lmflf  21018  txflf  21019  fclsopn  21027  fclsfnflim  21040  alexsublem  21057  ptcmplem3  21067  cnextcn  21080  symgtgp  21114  submtmd  21117  subgtgp  21118  clssubg  21121  clsnsg  21122  tgpconcompeqg  21124  snclseqg  21128  tsmscls  21150  trust  21242  restutop  21250  restutopopn  21251  utop3cls  21264  utopreg  21265  trcfilu  21307  blssec  21448  prdsbl  21504  blssopn  21508  metcnp  21554  cfilucfil  21572  psmetutop  21580  iccntr  21837  icccmplem2  21839  reconnlem1  21842  metnrmlem1a  21873  metnrmlem1  21874  metnrmlem2  21875  metnrmlem3  21876  metnrmlem1aOLD  21888  metnrmlem1OLD  21889  metnrmlem2OLD  21890  metnrmlem3OLD  21891  cnheibor  21981  lebnumlem1  21987  lebnumlem3  21989  lebnumlem1OLD  21990  lebnumlem3OLD  21992  lebnumii  21995  clsocv  22219  iscfil2  22234  iscmet3  22261  cmetss  22282  relcmpcmet  22284  bcthlem5  22294  itg1addlem5  22656  perfdvf  22856  dvres3  22866  dvres3a  22867  dvcmul  22896  dvcmulf  22897  dvlip2  22945  lhop1lem  22963  dvcnvrelem1  22967  dvcnvrelem2  22968  dvcnvre  22969  dvcvx  22970  plyco0  23144  plyaddlem1  23165  plymullem1  23166  aalioulem3  23288  ulmdvlem1  23353  axcontlem10  25001  eengtrkg  25013  eupares  25701  ghsubgolemOLD  26096  hsupunss  26994  pjpjpre  27070  ssmd2  27963  superpos  28005  atexch  28032  curry2ima  28291  madjusmdetlem2  28662  ordtconlem1  28738  measiuns  29047  imambfm  29092  cnmbfm  29093  dya2iocnrect  29111  omsfval  29126  omsfvalOLD  29130  omssubaddlem  29135  omssubadd  29136  omssubaddlemOLD  29139  omssubaddOLD  29140  totprobd  29267  fzssfzo  29430  signstfvn  29466  bnj999  29776  bnj1408  29853  bnj1442  29866  bnj1450  29867  bnj1501  29884  cvmsss2  30005  cvmliftmolem1  30012  cvmliftlem3  30018  cvmlift2lem9  30042  cvmlift2lem11  30044  cvmlift3lem6  30055  cvmlift3lem7  30056  ssmclslem  30211  mclsax  30215  mclsppslem  30229  mclspps  30230  dfrdg2  30449  trpredtr  30478  neiin  30993  neibastop2  31022  filnetlem4  31042  poimirlem11  31915  poimirlem12  31916  itg2addnclem2  31958  cnres2  32059  sstotbnd2  32070  sstotbnd  32071  prdstotbnd  32090  heibor1lem  32105  igenval2  32263  lshpnelb  32519  lcvexchlem4  32572  lsatexch  32578  l1cvat  32590  lkrscss  32633  lkrss  32703  lkreqN  32705  paddunN  33461  osumcllem2N  33491  pmapojoinN  33502  pl42lem2N  33514  dibglbN  34703  diblss  34707  dicvaddcl  34727  dicvscacl  34728  diclss  34730  cdlemn5pre  34737  dihord5apre  34799  dihglblem3N  34832  dihglb2  34879  dochsat  34920  dochshpncl  34921  djhspss  34943  dihsumssj  34945  mapdlsm  35201  hdmaprnlem3eN  35398  hdmaplkr  35453  fnwe2lem2  35879  lnmlsslnm  35909  lmhmfgima  35912  hbtlem6  35958  trrelsuperreldg  36230  iunrelexpuztr  36281  funfvima2d  36582  dvsconst  36649  dvsinax  37723  dvbdfbdioolem1  37740  itgsinexplem1  37770  itgperiod  37798  stoweidlem39  37840  dirkeritg  37904  fourierdlem48  37958  fourierdlem49  37959  fourierdlem70  37980  fourierdlem71  37981  fourierdlem81  37991  pfxccatin12  38836  nbumgruvtxres  39236  subsubmgm  39416  rmsuppss  39776
  Copyright terms: Public domain W3C validator