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

Theorem sseqtr4d 3392
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 2447 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3391 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3334  df-ss 3341
This theorem is referenced by:  syl5sseqr  3404  reusv6OLD  4502  fnfvima  5954  oaordi  6984  omordi  7004  omlimcl  7016  oen0  7024  domunsncan  7410  f1opwfi  7614  cantnfle  7878  cantnflt  7879  cantnflem1d  7895  cantnfleOLD  7908  cantnfltOLD  7909  cantnflem1dOLD  7918  r1pwss  7990  rankxplim3  8087  acndom2  8223  fodomfi2  8229  cflm  8418  cflim2  8431  isf34lem5  8546  isf34lem7  8547  isf34lem6  8548  axdc2lem  8616  ttukeylem5  8681  wunex2  8904  ccatass  12285  swrdval2  12315  swrdccatin12  12381  splfv2a  12397  revccat  12405  sumrblem  13187  dfphi2  13848  vdwlem1  14041  imasaddfnlem  14465  imasaddvallem  14466  imasvscafn  14474  imasvscaval  14475  mreexexlem4d  14584  mreexfidimd  14587  sscpwex  14727  acsmap2d  15348  subsubm  15484  gsumress  15506  frmdsssubm  15538  frmdss2  15540  subsubg  15703  cntzmhm2  15856  cntzcmnf  16326  ablcntzd  16338  gsumzsubmcl  16401  gsumzsubmclOLD  16402  gsumzmhm  16429  gsumzmhmOLD  16430  subgdmdprd  16530  dprdcntz2  16535  dprd2da  16540  dmdprdsplit2lem  16543  ablfac1eu  16573  pgpfaclem1  16581  pgpfaclem2  16582  issubdrg  16889  subsubrg  16890  lmhmlsp  17129  lspsntri  17177  lspindpi  17212  lidldvgen  17336  opsrtoslem2  17565  gsumfsum  17878  mrccss  18118  frlmsslsp  18222  frlmsslspOLD  18223  toponss  18533  ssntr  18661  elcls3  18686  toponmre  18696  neiptoptop  18734  neiptopnei  18735  neitr  18783  ordtbas  18795  ordtopn1  18797  ordtopn2  18798  iscnp3  18847  tgcn  18855  tgcnp  18856  ssidcn  18858  cnclsi  18875  cncls  18877  cncnp  18883  cnrest  18888  lmcld  18906  tgcmp  19003  cnconn  19025  conima  19028  clscon  19033  concompcld  19037  1stccnp  19065  kgentopon  19110  llycmpkgen2  19122  1stckgen  19126  kgencn2  19129  ptopn  19155  txcls  19176  ptpjcn  19183  ptclsg  19187  xkoccn  19191  txcnp  19192  ptcnplem  19193  txcmplem2  19214  xkoptsub  19226  xkopt  19227  xkoco2cn  19230  xkococnlem  19231  xkoinjcn  19259  imasnopn  19262  imasncld  19263  imasncls  19264  qtopkgen  19282  basqtop  19283  tgqtop  19284  qtoprest  19289  kqsat  19303  kqcldsat  19305  kqnrmlem1  19315  kqnrmlem2  19316  hmeontr  19341  reghmph  19365  nrmhmph  19366  fmfnfmlem4  19529  fmfnfm  19530  flimopn  19547  flimclslem  19556  flfnei  19563  lmflf  19577  txflf  19578  fclsopn  19586  fclsfnflim  19599  alexsublem  19615  ptcmplem3  19625  cnextcn  19638  symgtgp  19671  submtmd  19674  subgtgp  19675  clssubg  19678  clsnsg  19679  tgpconcompeqg  19681  snclseqg  19685  tsmscls  19707  trust  19803  restutop  19811  restutopopn  19812  utop3cls  19825  utopreg  19826  trcfilu  19868  blssec  20009  prdsbl  20065  blssopn  20069  metcnp  20115  cfilucfilOLD  20143  cfilucfil  20144  metutopOLD  20156  psmetutop  20157  iccntr  20397  icccmplem2  20399  reconnlem1  20402  metnrmlem1a  20433  metnrmlem1  20434  metnrmlem2  20435  metnrmlem3  20436  cnheibor  20526  lebnumlem1  20532  lebnumlem3  20534  lebnumii  20537  clsocv  20761  iscfil2  20776  iscmet3  20803  cmetss  20824  relcmpcmet  20826  bcthlem5  20838  itg1addlem5  21177  perfdvf  21377  dvres3  21387  dvres3a  21388  dvcmul  21417  dvcmulf  21418  dvlip2  21466  lhop1lem  21484  dvcnvrelem1  21488  dvcnvrelem2  21489  dvcnvre  21490  dvcvx  21491  plyco0  21659  plyaddlem1  21680  plymullem1  21681  aalioulem3  21799  ulmdvlem1  21864  axcontlem10  23218  eengtrkg  23230  eupares  23595  ghsubgolem  23856  hsupunss  24745  pjpjpre  24821  ssmd2  25715  superpos  25757  atexch  25784  curry2ima  26002  ordtconlem1  26353  measiuns  26630  imambfm  26676  cnmbfm  26677  dya2iocnrect  26695  sitgclg  26727  totprobd  26808  fzssfzo  26933  signstfvn  26969  cvmsss2  27162  cvmliftmolem1  27169  cvmliftlem3  27175  cvmlift2lem9  27199  cvmlift2lem11  27201  cvmlift3lem6  27212  cvmlift3lem7  27213  rtrclreclem.refl  27345  rtrclreclem.subset  27346  prodrblem  27441  dfrdg2  27608  trpredtr  27693  itg2addnclem2  28442  neiin  28525  neibastop2  28580  filnetlem4  28600  cnres2  28660  sstotbnd2  28671  sstotbnd  28672  prdstotbnd  28691  heibor1lem  28706  igenval2  28864  fnwe2lem2  29402  lnmlsslnm  29432  lmhmfgima  29435  hbtlem6  29483  dvsconst  29602  itgsinexplem1  29792  stoweidlem39  29832  rmsuppss  30781  scmatsgrp1  30887  bnj999  31948  bnj1408  32025  bnj1442  32038  bnj1450  32039  bnj1501  32056  lshpnelb  32627  lcvexchlem4  32680  lsatexch  32686  l1cvat  32698  lkrscss  32741  lkrss  32811  lkreqN  32813  paddunN  33569  osumcllem2N  33599  pmapojoinN  33610  pl42lem2N  33622  dibglbN  34809  diblss  34813  dicvaddcl  34833  dicvscacl  34834  diclss  34836  cdlemn5pre  34843  dihord5apre  34905  dihglblem3N  34938  dihglb2  34985  dochsat  35026  dochshpncl  35027  djhspss  35049  dihsumssj  35051  mapdlsm  35307  hdmaprnlem3eN  35504  hdmaplkr  35559
  Copyright terms: Public domain W3C validator