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

Theorem sseqtr4d 3385
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 2441 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3384 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3320
This theorem is referenced by:  syl5sseqr  3397  reusv6OLD  4734  fnfvima  5976  oaordi  6789  omordi  6809  omlimcl  6821  oen0  6829  domunsncan  7208  f1opwfi  7410  cantnfle  7626  cantnflt  7627  cantnflem1d  7644  r1pwss  7710  rankxplim3  7805  acndom2  7935  fodomfi2  7941  cflm  8130  cflim2  8143  isf34lem5  8258  isf34lem7  8259  isf34lem6  8260  axdc2lem  8328  ttukeylem5  8393  wunex2  8613  ccatass  11750  swrdval2  11767  splfv2a  11785  revccat  11798  sumrblem  12505  dfphi2  13163  vdwlem1  13349  imasaddfnlem  13753  imasaddvallem  13754  imasvscafn  13762  imasvscaval  13763  mreexexlem4d  13872  mreexfidimd  13875  sscpwex  14015  acsmap2d  14605  subsubm  14757  gsumress  14777  frmdsssubm  14806  frmdss2  14808  subsubg  14963  cntzmhm2  15138  ablcntzd  15472  cntzcmnf  15515  gsumzsubmcl  15523  gsumzmhm  15533  subgdmdprd  15592  dprdcntz2  15596  dprd2da  15600  dmdprdsplit2lem  15603  ablfac1eu  15631  pgpfaclem1  15639  pgpfaclem2  15640  issubdrg  15893  subsubrg  15894  lmhmlsp  16125  lspsntri  16169  lspindpi  16204  lidldvgen  16326  opsrtoslem2  16545  gsumfsum  16766  mrccss  16921  toponss  16994  ssntr  17122  elcls3  17147  toponmre  17157  neiptoptop  17195  neiptopnei  17196  neitr  17244  ordtbas  17256  ordtopn1  17258  ordtopn2  17259  iscnp3  17308  tgcn  17316  tgcnp  17317  ssidcn  17319  cnclsi  17336  cncls  17338  cncnp  17344  cnrest  17349  lmcld  17367  tgcmp  17464  cnconn  17485  conima  17488  clscon  17493  concompcld  17497  1stccnp  17525  kgentopon  17570  llycmpkgen2  17582  1stckgen  17586  kgencn2  17589  ptopn  17615  txcls  17636  ptpjcn  17643  ptclsg  17647  xkoccn  17651  txcnp  17652  ptcnplem  17653  txcmplem2  17674  xkoptsub  17686  xkopt  17687  xkoco2cn  17690  xkococnlem  17691  xkoinjcn  17719  imasnopn  17722  imasncld  17723  imasncls  17724  qtopkgen  17742  basqtop  17743  tgqtop  17744  qtoprest  17749  kqsat  17763  kqcldsat  17765  kqnrmlem1  17775  kqnrmlem2  17776  hmeontr  17801  reghmph  17825  nrmhmph  17826  fmfnfmlem4  17989  fmfnfm  17990  flimopn  18007  flimclslem  18016  flfnei  18023  lmflf  18037  txflf  18038  fclsopn  18046  fclsfnflim  18059  alexsublem  18075  ptcmplem3  18085  cnextcn  18098  symgtgp  18131  submtmd  18134  subgtgp  18135  clssubg  18138  clsnsg  18139  tgpconcompeqg  18141  snclseqg  18145  tsmscls  18167  trust  18259  restutop  18267  restutopopn  18268  utop3cls  18281  utopreg  18282  trcfilu  18324  blssec  18465  prdsbl  18521  blssopn  18525  metcnp  18571  cfilucfilOLD  18599  cfilucfil  18600  metutopOLD  18612  psmetutop  18613  iccntr  18852  icccmplem2  18854  reconnlem1  18857  metnrmlem1a  18888  metnrmlem1  18889  metnrmlem2  18890  metnrmlem3  18891  cnheibor  18980  lebnumlem1  18986  lebnumlem3  18988  lebnumii  18991  clsocv  19204  iscfil2  19219  iscmet3  19246  cmetss  19267  relcmpcmet  19269  bcthlem5  19281  itg1addlem5  19592  perfdvf  19790  dvres3  19800  dvres3a  19801  dvcmul  19830  dvcmulf  19831  dvlip2  19879  lhop1lem  19897  dvcnvrelem1  19901  dvcnvrelem2  19902  dvcnvre  19903  dvcvx  19904  plyco0  20111  plyaddlem1  20132  plymullem1  20133  aalioulem3  20251  ulmdvlem1  20316  eupares  21697  ghsubgolem  21958  hsupunss  22845  pjpjpre  22921  ssmd2  23815  superpos  23857  atexch  23884  curry2ima  24097  measiuns  24571  imambfm  24612  cnmbfm  24613  dya2iocnrect  24631  sitgclg  24656  totprobd  24684  cvmsss2  24961  cvmliftmolem1  24968  cvmliftlem3  24974  cvmlift2lem9  24998  cvmlift2lem11  25000  cvmlift3lem6  25011  cvmlift3lem7  25012  rtrclreclem.refl  25144  rtrclreclem.subset  25145  prodrblem  25255  dfrdg2  25423  trpredtr  25508  axcontlem10  25912  itg2addnclem2  26257  neiin  26335  neibastop2  26390  filnetlem4  26410  cnres2  26472  sstotbnd2  26483  sstotbnd  26484  prdstotbnd  26503  heibor1lem  26518  igenval2  26676  fnwe2lem2  27126  lnmlsslnm  27156  lmhmfgima  27159  frlmsslsp  27225  hbtlem6  27310  dvsconst  27524  itgsinexplem1  27724  stoweidlem39  27764  swrdccatin12  28214  bnj999  29328  bnj1408  29405  bnj1442  29418  bnj1450  29419  bnj1501  29436  lshpnelb  29782  lcvexchlem4  29835  lsatexch  29841  l1cvat  29853  lkrscss  29896  lkrss  29966  lkreqN  29968  paddunN  30724  osumcllem2N  30754  pmapojoinN  30765  pl42lem2N  30777  dibglbN  31964  diblss  31968  dicvaddcl  31988  dicvscacl  31989  diclss  31991  cdlemn5pre  31998  dihord5apre  32060  dihglblem3N  32093  dihglb2  32140  dochsat  32181  dochshpncl  32182  djhspss  32204  dihsumssj  32206  mapdlsm  32462  hdmaprnlem3eN  32659  hdmaplkr  32714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator