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

Theorem sseqtr4d 3345
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 2409 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3344 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3280
This theorem is referenced by:  syl5sseqr  3357  reusv6OLD  4693  fnfvima  5935  oaordi  6748  omordi  6768  omlimcl  6780  oen0  6788  domunsncan  7167  f1opwfi  7368  cantnfle  7582  cantnflt  7583  cantnflem1d  7600  r1pwss  7666  rankxplim3  7761  acndom2  7891  fodomfi2  7897  cflm  8086  cflim2  8099  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  axdc2lem  8284  ttukeylem5  8349  wunex2  8569  ccatass  11705  swrdval2  11722  splfv2a  11740  revccat  11753  sumrblem  12460  dfphi2  13118  vdwlem1  13304  imasaddfnlem  13708  imasaddvallem  13709  imasvscafn  13717  imasvscaval  13718  mreexexlem4d  13827  mreexfidimd  13830  sscpwex  13970  acsmap2d  14560  subsubm  14712  gsumress  14732  frmdsssubm  14761  frmdss2  14763  subsubg  14918  cntzmhm2  15093  ablcntzd  15427  cntzcmnf  15470  gsumzsubmcl  15478  gsumzmhm  15488  subgdmdprd  15547  dprdcntz2  15551  dprd2da  15555  dmdprdsplit2lem  15558  ablfac1eu  15586  pgpfaclem1  15594  pgpfaclem2  15595  issubdrg  15848  subsubrg  15849  lmhmlsp  16080  lspsntri  16124  lspindpi  16159  lidldvgen  16281  opsrtoslem2  16500  gsumfsum  16721  mrccss  16876  toponss  16949  ssntr  17077  elcls3  17102  toponmre  17112  neiptoptop  17150  neiptopnei  17151  neitr  17198  ordtbas  17210  ordtopn1  17212  ordtopn2  17213  iscnp3  17262  tgcn  17270  tgcnp  17271  ssidcn  17273  cnclsi  17290  cncls  17292  cncnp  17298  cnrest  17303  lmcld  17321  tgcmp  17418  cnconn  17438  conima  17441  clscon  17446  concompcld  17450  1stccnp  17478  kgentopon  17523  llycmpkgen2  17535  1stckgen  17539  kgencn2  17542  ptopn  17568  txcls  17589  ptpjcn  17596  ptclsg  17600  xkoccn  17604  txcnp  17605  ptcnplem  17606  txcmplem2  17627  xkoptsub  17639  xkopt  17640  xkoco2cn  17643  xkococnlem  17644  xkoinjcn  17672  imasnopn  17675  imasncld  17676  imasncls  17677  qtopkgen  17695  basqtop  17696  tgqtop  17697  qtoprest  17702  kqsat  17716  kqcldsat  17718  kqnrmlem1  17728  kqnrmlem2  17729  hmeontr  17754  reghmph  17778  nrmhmph  17779  fmfnfmlem4  17942  fmfnfm  17943  flimopn  17960  flimclslem  17969  flfnei  17976  lmflf  17990  txflf  17991  fclsopn  17999  fclsfnflim  18012  alexsublem  18028  ptcmplem3  18038  cnextcn  18051  symgtgp  18084  submtmd  18087  subgtgp  18088  clssubg  18091  clsnsg  18092  tgpconcompeqg  18094  snclseqg  18098  tsmscls  18120  trust  18212  restutop  18220  restutopopn  18221  utop3cls  18234  utopreg  18235  trcfilu  18277  blssec  18418  prdsbl  18474  blssopn  18478  metcnp  18524  cfilucfilOLD  18552  cfilucfil  18553  metutopOLD  18565  psmetutop  18566  iccntr  18805  icccmplem2  18807  reconnlem1  18810  metnrmlem1a  18841  metnrmlem1  18842  metnrmlem2  18843  metnrmlem3  18844  cnheibor  18933  lebnumlem1  18939  lebnumlem3  18941  lebnumii  18944  clsocv  19157  iscfil2  19172  iscmet3  19199  cmetss  19220  relcmpcmet  19222  bcthlem5  19234  itg1addlem5  19545  perfdvf  19743  dvres3  19753  dvres3a  19754  dvcmul  19783  dvcmulf  19784  dvlip2  19832  lhop1lem  19850  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  dvcvx  19857  plyco0  20064  plyaddlem1  20085  plymullem1  20086  aalioulem3  20204  ulmdvlem1  20269  eupares  21650  ghsubgolem  21911  hsupunss  22798  pjpjpre  22874  ssmd2  23768  superpos  23810  atexch  23837  curry2ima  24050  measiuns  24524  imambfm  24565  cnmbfm  24566  dya2iocnrect  24584  sitgclg  24609  totprobd  24637  cvmsss2  24914  cvmliftmolem1  24921  cvmliftlem3  24927  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift3lem6  24964  cvmlift3lem7  24965  rtrclreclem.refl  25097  rtrclreclem.subset  25098  prodrblem  25208  dfrdg2  25366  trpredtr  25447  axcontlem10  25816  itg2addnclem2  26156  neiin  26225  neibastop2  26280  filnetlem4  26300  cnres2  26362  sstotbnd2  26373  sstotbnd  26374  prdstotbnd  26393  heibor1lem  26408  igenval2  26566  fnwe2lem2  27016  lnmlsslnm  27047  lmhmfgima  27050  frlmsslsp  27116  hbtlem6  27201  dvsconst  27415  itgsinexplem1  27615  stoweidlem39  27655  bnj999  29034  bnj1408  29111  bnj1442  29124  bnj1450  29125  bnj1501  29142  lshpnelb  29467  lcvexchlem4  29520  lsatexch  29526  l1cvat  29538  lkrscss  29581  lkrss  29651  lkreqN  29653  paddunN  30409  osumcllem2N  30439  pmapojoinN  30450  pl42lem2N  30462  dibglbN  31649  diblss  31653  dicvaddcl  31673  dicvscacl  31674  diclss  31676  cdlemn5pre  31683  dihord5apre  31745  dihglblem3N  31778  dihglb2  31825  dochsat  31866  dochshpncl  31867  djhspss  31889  dihsumssj  31891  mapdlsm  32147  hdmaprnlem3eN  32344  hdmaplkr  32399
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator