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

Theorem sseqtr4d 3228
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 2301 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3227 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  syl5sseqr  3240  reusv6OLD  4561  fnfvima  5772  oaordi  6560  omordi  6580  omlimcl  6592  oen0  6600  domunsncan  6978  f1opwfi  7175  cantnfle  7388  cantnflt  7389  cantnflem1d  7406  r1pwss  7472  rankxplim3  7567  acndom2  7697  fodomfi2  7703  cflm  7892  cflim2  7905  isf34lem5  8020  isf34lem7  8021  isf34lem6  8022  axdc2lem  8090  ttukeylem5  8156  wunex2  8376  ccatass  11452  swrdval2  11469  splfv2a  11487  revccat  11500  sumrblem  12200  dfphi2  12858  vdwlem1  13044  imasaddfnlem  13446  imasaddvallem  13447  imasvscafn  13455  imasvscaval  13456  mreexexlem4d  13565  mreexfidimd  13568  sscpwex  13708  acsmap2d  14298  subsubm  14450  gsumress  14470  frmdsssubm  14499  frmdss2  14501  subsubg  14656  cntzmhm2  14831  ablcntzd  15165  cntzcmnf  15208  gsumzsubmcl  15216  gsumzmhm  15226  subgdmdprd  15285  dprdcntz2  15289  dprd2da  15293  dmdprdsplit2lem  15296  ablfac1eu  15324  pgpfaclem1  15332  pgpfaclem2  15333  issubdrg  15586  subsubrg  15587  lmhmlsp  15822  lspsntri  15866  lspindpi  15901  lidldvgen  16023  opsrtoslem2  16242  gsumfsum  16455  mrccss  16610  toponss  16683  ssntr  16811  elcls3  16836  toponmre  16846  ordtbas  16938  ordtopn1  16940  ordtopn2  16941  iscnp3  16990  tgcn  16998  tgcnp  16999  ssidcn  17001  cnclsi  17017  cncls  17019  cncnp  17025  cnrest  17029  lmcld  17047  tgcmp  17144  cnconn  17164  conima  17167  clscon  17172  concompcld  17176  1stccnp  17204  kgentopon  17249  llycmpkgen2  17261  1stckgen  17265  kgencn2  17268  ptopn  17294  txcls  17315  ptpjcn  17321  ptclsg  17325  xkoccn  17329  txcnp  17330  ptcnplem  17331  txcmplem2  17352  xkoptsub  17364  xkopt  17365  xkoco2cn  17368  xkococnlem  17369  xkoinjcn  17397  qtopkgen  17417  basqtop  17418  tgqtop  17419  qtoprest  17424  kqsat  17438  kqcldsat  17440  kqnrmlem1  17450  kqnrmlem2  17451  hmeontr  17476  reghmph  17500  nrmhmph  17501  fmfnfmlem4  17668  fmfnfm  17669  flimopn  17686  flimclslem  17695  flfnei  17702  lmflf  17716  txflf  17717  fclsopn  17725  fclsfnflim  17738  alexsublem  17754  ptcmplem3  17764  symgtgp  17800  submtmd  17803  subgtgp  17804  clssubg  17807  clsnsg  17808  tgpconcompeqg  17810  snclseqg  17814  tsmscls  17836  blssec  17997  prdsbl  18053  blssopn  18057  metcnp  18103  iccntr  18342  icccmplem2  18344  reconnlem1  18347  metnrmlem1a  18378  metnrmlem1  18379  metnrmlem2  18380  metnrmlem3  18381  cnheibor  18469  lebnumlem1  18475  lebnumlem3  18477  lebnumii  18480  clsocv  18693  iscfil2  18708  iscmet3  18735  cmetss  18756  relcmpcmet  18758  bcthlem5  18766  itg1addlem5  19071  perfdvf  19269  dvres3  19279  dvres3a  19280  dvcmul  19309  dvcmulf  19310  dvlip2  19358  lhop1lem  19376  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  dvcvx  19383  plyco0  19590  plyaddlem1  19611  plymullem1  19612  aalioulem3  19730  ulmdvlem1  19793  ghsubgolem  21053  hsupunss  21938  pjpjpre  22014  ssmd2  22908  superpos  22950  atexch  22977  ofrn2  23222  curry2ima  23262  measiuns  23559  imambfm  23582  cnmbfm  23583  totprobd  23644  cvmsss2  23820  cvmliftmolem1  23827  cvmliftlem3  23833  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift3lem6  23870  cvmlift3lem7  23871  eupares  23914  rtrclreclem.refl  24056  rtrclreclem.subset  24057  prodrblem  24152  dfrdg2  24223  trpredtr  24304  axcontlem10  24673  itg2addnclem2  25004  cmptdst  25671  flfnei2  25680  lvsovso  25729  tartarmap  25991  setiscat  26082  xindcls  26100  neiin  26353  neibastop2  26413  filnetlem4  26433  cnres2  26586  sstotbnd2  26601  sstotbnd  26602  prdstotbnd  26621  heibor1lem  26636  igenval2  26794  fnwe2lem2  27251  lnmlsslnm  27282  lmhmfgima  27285  frlmsslsp  27351  hbtlem6  27436  dvsconst  27650  itgsinexplem1  27851  stoweidlem39  27891  bnj999  29305  bnj1408  29382  bnj1442  29395  bnj1450  29396  bnj1501  29413  lshpnelb  29796  lcvexchlem4  29849  lsatexch  29855  l1cvat  29867  lkrscss  29910  lkrss  29980  lkreqN  29982  paddunN  30738  osumcllem2N  30768  pmapojoinN  30779  pl42lem2N  30791  dibglbN  31978  diblss  31982  dicvaddcl  32002  dicvscacl  32003  diclss  32005  cdlemn5pre  32012  dihord5apre  32074  dihglblem3N  32107  dihglb2  32154  dochsat  32195  dochshpncl  32196  djhspss  32218  dihsumssj  32220  mapdlsm  32476  hdmaprnlem3eN  32673  hdmaplkr  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator