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

Theorem sseqtr4d 3526
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 2451 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3525 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  syl5sseqr  3538  reusv6OLD  4648  fnfvima  6135  oaordi  7197  omordi  7217  omlimcl  7229  oen0  7237  domunsncan  7619  f1opwfi  7826  cantnfle  8093  cantnflt  8094  cantnflem1d  8110  cantnfleOLD  8123  cantnfltOLD  8124  cantnflem1dOLD  8133  r1pwss  8205  rankxplim3  8302  acndom2  8438  fodomfi2  8444  cflm  8633  cflim2  8646  isf34lem5  8761  isf34lem7  8762  isf34lem6  8763  axdc2lem  8831  ttukeylem5  8896  wunex2  9119  ccatass  12587  swrdval2  12629  swrdccatin12  12698  splfv2a  12714  revccat  12722  sumrblem  13515  prodrblem  13718  dfphi2  14286  vdwlem1  14481  imasaddfnlem  14907  imasaddvallem  14908  imasvscafn  14916  imasvscaval  14917  mreexexlem4d  15026  mreexfidimd  15029  sscpwex  15166  acsmap2d  15788  gsumress  15882  subsubm  15967  frmdsssubm  16008  frmdss2  16010  subsubg  16203  cntzmhm2  16356  cntzcmnf  16830  ablcntzd  16842  gsumzsubmcl  16907  gsumzsubmclOLD  16908  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  gsumzoppg  16946  subgdmdprd  17060  dprdcntz2  17065  dprd2da  17070  dmdprdsplit2lem  17073  ablfac1eu  17103  pgpfaclem1  17111  pgpfaclem2  17112  issubdrg  17433  subsubrg  17434  lmhmlsp  17674  lspsntri  17722  lspindpi  17757  lidldvgen  17882  opsrtoslem2  18128  gsumfsum  18463  mrccss  18703  frlmsslsp  18807  frlmsslspOLD  18808  scmatsgrp1  19002  toponss  19408  ssntr  19537  elcls3  19562  toponmre  19572  neiptoptop  19610  neiptopnei  19611  neitr  19659  ordtbas  19671  ordtopn1  19673  ordtopn2  19674  iscnp3  19723  tgcn  19731  tgcnp  19732  ssidcn  19734  cnclsi  19751  cncls  19753  cncnp  19759  lmcld  19782  tgcmp  19879  cnconn  19901  conima  19904  clscon  19909  concompcld  19913  1stccnp  19941  kgentopon  20017  llycmpkgen2  20029  1stckgen  20033  kgencn2  20036  ptopn  20062  txcls  20083  ptpjcn  20090  ptclsg  20094  xkoccn  20098  txcnp  20099  ptcnplem  20100  txcmplem2  20121  xkoptsub  20133  xkopt  20134  xkoco2cn  20137  xkococnlem  20138  xkoinjcn  20166  imasnopn  20169  imasncld  20170  imasncls  20171  qtopkgen  20189  basqtop  20190  tgqtop  20191  qtoprest  20196  kqsat  20210  kqcldsat  20212  kqnrmlem1  20222  kqnrmlem2  20223  hmeontr  20248  reghmph  20272  nrmhmph  20273  fmfnfmlem4  20436  fmfnfm  20437  flimopn  20454  flimclslem  20463  flfnei  20470  lmflf  20484  txflf  20485  fclsopn  20493  fclsfnflim  20506  alexsublem  20522  ptcmplem3  20532  cnextcn  20545  symgtgp  20578  submtmd  20581  subgtgp  20582  clssubg  20585  clsnsg  20586  tgpconcompeqg  20588  snclseqg  20592  tsmscls  20614  trust  20710  restutop  20718  restutopopn  20719  utop3cls  20732  utopreg  20733  trcfilu  20775  blssec  20916  prdsbl  20972  blssopn  20976  metcnp  21022  cfilucfilOLD  21050  cfilucfil  21051  metutopOLD  21063  psmetutop  21064  iccntr  21304  icccmplem2  21306  reconnlem1  21309  metnrmlem1a  21340  metnrmlem1  21341  metnrmlem2  21342  metnrmlem3  21343  cnheibor  21433  lebnumlem1  21439  lebnumlem3  21441  lebnumii  21444  clsocv  21668  iscfil2  21683  iscmet3  21710  cmetss  21731  relcmpcmet  21733  bcthlem5  21745  itg1addlem5  22085  perfdvf  22285  dvres3  22295  dvres3a  22296  dvcmul  22325  dvcmulf  22326  dvlip2  22374  lhop1lem  22392  dvcnvrelem1  22396  dvcnvrelem2  22397  dvcnvre  22398  dvcvx  22399  plyco0  22567  plyaddlem1  22588  plymullem1  22589  aalioulem3  22708  ulmdvlem1  22773  axcontlem10  24254  eengtrkg  24266  eupares  24953  ghsubgolemOLD  25350  hsupunss  26239  pjpjpre  26315  ssmd2  27209  superpos  27251  atexch  27278  curry2ima  27504  ordtconlem1  27884  measiuns  28166  imambfm  28211  cnmbfm  28212  dya2iocnrect  28230  totprobd  28343  fzssfzo  28468  signstfvn  28504  cvmsss2  28697  cvmliftmolem1  28704  cvmliftlem3  28710  cvmlift2lem9  28734  cvmlift2lem11  28736  cvmlift3lem6  28747  cvmlift3lem7  28748  ssmclslem  28903  mclsax  28907  mclsppslem  28921  mclspps  28922  rtrclreclem.refl  29045  rtrclreclem.subset  29046  dfrdg2  29204  trpredtr  29289  itg2addnclem2  30043  neiin  30126  neibastop2  30155  filnetlem4  30175  cnres2  30235  sstotbnd2  30246  sstotbnd  30247  prdstotbnd  30266  heibor1lem  30281  igenval2  30439  fnwe2lem2  30973  lnmlsslnm  31003  lmhmfgima  31006  hbtlem6  31054  dvsconst  31211  dvsinax  31662  dvbdfbdioolem1  31679  itgsinexplem1  31706  itgperiod  31734  stoweidlem39  31775  dirkeritg  31838  fourierdlem48  31891  fourierdlem49  31892  fourierdlem70  31913  fourierdlem71  31914  fourierdlem81  31924  subsubmgm  32439  rmsuppss  32833  bnj999  33883  bnj1408  33960  bnj1442  33973  bnj1450  33974  bnj1501  33991  lshpnelb  34584  lcvexchlem4  34637  lsatexch  34643  l1cvat  34655  lkrscss  34698  lkrss  34768  lkreqN  34770  paddunN  35526  osumcllem2N  35556  pmapojoinN  35567  pl42lem2N  35579  dibglbN  36768  diblss  36772  dicvaddcl  36792  dicvscacl  36793  diclss  36795  cdlemn5pre  36802  dihord5apre  36864  dihglblem3N  36897  dihglb2  36944  dochsat  36985  dochshpncl  36986  djhspss  37008  dihsumssj  37010  mapdlsm  37266  hdmaprnlem3eN  37463  hdmaplkr  37518  trrelsuperreldg  37611  funfvima2d  37790
  Copyright terms: Public domain W3C validator