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

Theorem sseqtr4d 3541
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 2475 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3540 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  syl5sseqr  3553  reusv6OLD  4658  fnfvima  6138  oaordi  7195  omordi  7215  omlimcl  7227  oen0  7235  domunsncan  7617  f1opwfi  7824  cantnfle  8090  cantnflt  8091  cantnflem1d  8107  cantnfleOLD  8120  cantnfltOLD  8121  cantnflem1dOLD  8130  r1pwss  8202  rankxplim3  8299  acndom2  8435  fodomfi2  8441  cflm  8630  cflim2  8643  isf34lem5  8758  isf34lem7  8759  isf34lem6  8760  axdc2lem  8828  ttukeylem5  8893  wunex2  9116  ccatass  12570  swrdval2  12610  swrdccatin12  12679  splfv2a  12695  revccat  12703  sumrblem  13496  dfphi2  14163  vdwlem1  14358  imasaddfnlem  14783  imasaddvallem  14784  imasvscafn  14792  imasvscaval  14793  mreexexlem4d  14902  mreexfidimd  14905  sscpwex  15045  acsmap2d  15666  subsubm  15807  gsumress  15829  frmdsssubm  15861  frmdss2  15863  subsubg  16029  cntzmhm2  16182  cntzcmnf  16654  ablcntzd  16666  gsumzsubmcl  16731  gsumzsubmclOLD  16732  gsumzmhm  16760  gsumzmhmOLD  16761  subgdmdprd  16883  dprdcntz2  16888  dprd2da  16893  dmdprdsplit2lem  16896  ablfac1eu  16926  pgpfaclem1  16934  pgpfaclem2  16935  issubdrg  17254  subsubrg  17255  lmhmlsp  17495  lspsntri  17543  lspindpi  17578  lidldvgen  17702  opsrtoslem2  17948  gsumfsum  18280  mrccss  18520  frlmsslsp  18624  frlmsslspOLD  18625  scmatsgrp1  18819  toponss  19225  ssntr  19353  elcls3  19378  toponmre  19388  neiptoptop  19426  neiptopnei  19427  neitr  19475  ordtbas  19487  ordtopn1  19489  ordtopn2  19490  iscnp3  19539  tgcn  19547  tgcnp  19548  ssidcn  19550  cnclsi  19567  cncls  19569  cncnp  19575  cnrest  19580  lmcld  19598  tgcmp  19695  cnconn  19717  conima  19720  clscon  19725  concompcld  19729  1stccnp  19757  kgentopon  19802  llycmpkgen2  19814  1stckgen  19818  kgencn2  19821  ptopn  19847  txcls  19868  ptpjcn  19875  ptclsg  19879  xkoccn  19883  txcnp  19884  ptcnplem  19885  txcmplem2  19906  xkoptsub  19918  xkopt  19919  xkoco2cn  19922  xkococnlem  19923  xkoinjcn  19951  imasnopn  19954  imasncld  19955  imasncls  19956  qtopkgen  19974  basqtop  19975  tgqtop  19976  qtoprest  19981  kqsat  19995  kqcldsat  19997  kqnrmlem1  20007  kqnrmlem2  20008  hmeontr  20033  reghmph  20057  nrmhmph  20058  fmfnfmlem4  20221  fmfnfm  20222  flimopn  20239  flimclslem  20248  flfnei  20255  lmflf  20269  txflf  20270  fclsopn  20278  fclsfnflim  20291  alexsublem  20307  ptcmplem3  20317  cnextcn  20330  symgtgp  20363  submtmd  20366  subgtgp  20367  clssubg  20370  clsnsg  20371  tgpconcompeqg  20373  snclseqg  20377  tsmscls  20399  trust  20495  restutop  20503  restutopopn  20504  utop3cls  20517  utopreg  20518  trcfilu  20560  blssec  20701  prdsbl  20757  blssopn  20761  metcnp  20807  cfilucfilOLD  20835  cfilucfil  20836  metutopOLD  20848  psmetutop  20849  iccntr  21089  icccmplem2  21091  reconnlem1  21094  metnrmlem1a  21125  metnrmlem1  21126  metnrmlem2  21127  metnrmlem3  21128  cnheibor  21218  lebnumlem1  21224  lebnumlem3  21226  lebnumii  21229  clsocv  21453  iscfil2  21468  iscmet3  21495  cmetss  21516  relcmpcmet  21518  bcthlem5  21530  itg1addlem5  21870  perfdvf  22070  dvres3  22080  dvres3a  22081  dvcmul  22110  dvcmulf  22111  dvlip2  22159  lhop1lem  22177  dvcnvrelem1  22181  dvcnvrelem2  22182  dvcnvre  22183  dvcvx  22184  plyco0  22352  plyaddlem1  22373  plymullem1  22374  aalioulem3  22492  ulmdvlem1  22557  axcontlem10  23980  eengtrkg  23992  eupares  24679  ghsubgolem  25076  hsupunss  25965  pjpjpre  26041  ssmd2  26935  superpos  26977  atexch  27004  curry2ima  27226  ordtconlem1  27570  measiuns  27856  imambfm  27901  cnmbfm  27902  dya2iocnrect  27920  totprobd  28033  fzssfzo  28158  signstfvn  28194  cvmsss2  28387  cvmliftmolem1  28394  cvmliftlem3  28400  cvmlift2lem9  28424  cvmlift2lem11  28426  cvmlift3lem6  28437  cvmlift3lem7  28438  rtrclreclem.refl  28570  rtrclreclem.subset  28571  prodrblem  28666  dfrdg2  28833  trpredtr  28918  itg2addnclem2  29672  neiin  29755  neibastop2  29810  filnetlem4  29830  cnres2  29890  sstotbnd2  29901  sstotbnd  29902  prdstotbnd  29921  heibor1lem  29936  igenval2  30094  fnwe2lem2  30629  lnmlsslnm  30659  lmhmfgima  30662  hbtlem6  30710  dvsconst  30863  itgsinexplem1  31299  iblsplit  31312  stoweidlem39  31367  dirkeritg  31430  dirkercncflem2  31432  fourierdlem81  31516  rmsuppss  32062  bnj999  33112  bnj1408  33189  bnj1442  33202  bnj1450  33203  bnj1501  33220  lshpnelb  33799  lcvexchlem4  33852  lsatexch  33858  l1cvat  33870  lkrscss  33913  lkrss  33983  lkreqN  33985  paddunN  34741  osumcllem2N  34771  pmapojoinN  34782  pl42lem2N  34794  dibglbN  35981  diblss  35985  dicvaddcl  36005  dicvscacl  36006  diclss  36008  cdlemn5pre  36015  dihord5apre  36077  dihglblem3N  36110  dihglb2  36157  dochsat  36198  dochshpncl  36199  djhspss  36221  dihsumssj  36223  mapdlsm  36479  hdmaprnlem3eN  36676  hdmaplkr  36731  trrelsuperreldg  36811
  Copyright terms: Public domain W3C validator