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

Theorem sseqtr4d 3215
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 2288 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3214 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  syl5sseqr  3227  reusv6OLD  4545  fnfvima  5756  oaordi  6544  omordi  6564  omlimcl  6576  oen0  6584  domunsncan  6962  f1opwfi  7159  cantnfle  7372  cantnflt  7373  cantnflem1d  7390  r1pwss  7456  rankxplim3  7551  acndom2  7681  fodomfi2  7687  cflm  7876  cflim2  7889  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  axdc2lem  8074  ttukeylem5  8140  wunex2  8360  ccatass  11436  swrdval2  11453  splfv2a  11471  revccat  11484  sumrblem  12184  dfphi2  12842  vdwlem1  13028  imasaddfnlem  13430  imasaddvallem  13431  imasvscafn  13439  imasvscaval  13440  mreexexlem4d  13549  mreexfidimd  13552  sscpwex  13692  acsmap2d  14282  subsubm  14434  gsumress  14454  frmdsssubm  14483  frmdss2  14485  subsubg  14640  cntzmhm2  14815  ablcntzd  15149  cntzcmnf  15192  gsumzsubmcl  15200  gsumzmhm  15210  subgdmdprd  15269  dprdcntz2  15273  dprd2da  15277  dmdprdsplit2lem  15280  ablfac1eu  15308  pgpfaclem1  15316  pgpfaclem2  15317  issubdrg  15570  subsubrg  15571  lmhmlsp  15806  lspsntri  15850  lspindpi  15885  lidldvgen  16007  opsrtoslem2  16226  gsumfsum  16439  mrccss  16594  toponss  16667  ssntr  16795  elcls3  16820  toponmre  16830  ordtbas  16922  ordtopn1  16924  ordtopn2  16925  iscnp3  16974  tgcn  16982  tgcnp  16983  ssidcn  16985  cnclsi  17001  cncls  17003  cncnp  17009  cnrest  17013  lmcld  17031  tgcmp  17128  cnconn  17148  conima  17151  clscon  17156  concompcld  17160  1stccnp  17188  kgentopon  17233  llycmpkgen2  17245  1stckgen  17249  kgencn2  17252  ptopn  17278  txcls  17299  ptpjcn  17305  ptclsg  17309  xkoccn  17313  txcnp  17314  ptcnplem  17315  txcmplem2  17336  xkoptsub  17348  xkopt  17349  xkoco2cn  17352  xkococnlem  17353  xkoinjcn  17381  qtopkgen  17401  basqtop  17402  tgqtop  17403  qtoprest  17408  kqsat  17422  kqcldsat  17424  kqnrmlem1  17434  kqnrmlem2  17435  hmeontr  17460  reghmph  17484  nrmhmph  17485  fmfnfmlem4  17652  fmfnfm  17653  flimopn  17670  flimclslem  17679  flfnei  17686  lmflf  17700  txflf  17701  fclsopn  17709  fclsfnflim  17722  alexsublem  17738  ptcmplem3  17748  symgtgp  17784  submtmd  17787  subgtgp  17788  clssubg  17791  clsnsg  17792  tgpconcompeqg  17794  snclseqg  17798  tsmscls  17820  blssec  17981  prdsbl  18037  blssopn  18041  metcnp  18087  iccntr  18326  icccmplem2  18328  reconnlem1  18331  metnrmlem1a  18362  metnrmlem1  18363  metnrmlem2  18364  metnrmlem3  18365  cnheibor  18453  lebnumlem1  18459  lebnumlem3  18461  lebnumii  18464  clsocv  18677  iscfil2  18692  iscmet3  18719  cmetss  18740  relcmpcmet  18742  bcthlem5  18750  itg1addlem5  19055  perfdvf  19253  dvres3  19263  dvres3a  19264  dvcmul  19293  dvcmulf  19294  dvlip2  19342  lhop1lem  19360  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  dvcvx  19367  plyco0  19574  plyaddlem1  19595  plymullem1  19596  aalioulem3  19714  ulmdvlem1  19777  ghsubgolem  21037  hsupunss  21922  pjpjpre  21998  ssmd2  22892  superpos  22934  atexch  22961  ofrn2  23207  curry2ima  23247  measiuns  23544  imambfm  23567  cnmbfm  23568  totprobd  23629  cvmsss2  23805  cvmliftmolem1  23812  cvmliftlem3  23818  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift3lem6  23855  cvmlift3lem7  23856  eupares  23899  rtrclreclem.refl  24041  rtrclreclem.subset  24042  dfrdg2  24152  trpredtr  24233  axcontlem10  24601  cmptdst  25568  flfnei2  25577  lvsovso  25626  tartarmap  25888  setiscat  25979  xindcls  25997  neiin  26250  neibastop2  26310  filnetlem4  26330  cnres2  26483  sstotbnd2  26498  sstotbnd  26499  prdstotbnd  26518  heibor1lem  26533  igenval2  26691  fnwe2lem2  27148  lnmlsslnm  27179  lmhmfgima  27182  frlmsslsp  27248  hbtlem6  27333  dvsconst  27547  itgsinexplem1  27748  stoweidlem39  27788  bnj999  28989  bnj1408  29066  bnj1442  29079  bnj1450  29080  bnj1501  29097  lshpnelb  29174  lcvexchlem4  29227  lsatexch  29233  l1cvat  29245  lkrscss  29288  lkrss  29358  lkreqN  29360  paddunN  30116  osumcllem2N  30146  pmapojoinN  30157  pl42lem2N  30169  dibglbN  31356  diblss  31360  dicvaddcl  31380  dicvscacl  31381  diclss  31383  cdlemn5pre  31390  dihord5apre  31452  dihglblem3N  31485  dihglb2  31532  dochsat  31573  dochshpncl  31574  djhspss  31596  dihsumssj  31598  mapdlsm  31854  hdmaprnlem3eN  32051  hdmaplkr  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator