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

Theorem sseqtr4d 3507
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 2437 . 2  |-  ( ph  ->  B  =  C )
41, 3sseqtrd 3506 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  syl5sseqr  3519  fnfvima  6158  wfrlem17  7060  oaordi  7255  omordi  7275  omlimcl  7287  oen0  7295  domunsncan  7678  f1opwfi  7884  cantnfle  8175  cantnflt  8176  cantnflem1d  8192  r1pwss  8254  rankxplim3  8351  acndom2  8483  fodomfi2  8489  cflm  8678  cflim2  8691  isf34lem5  8806  isf34lem7  8807  isf34lem6  8808  axdc2lem  8876  ttukeylem5  8941  wunex2  9162  ccatass  12719  swrdval2  12761  swrdccatin12  12832  splfv2a  12848  revccat  12856  rtrclreclem1  13100  rtrclreclem2  13101  sumrblem  13755  prodrblem  13961  dfphi2  14691  vdwlem1  14894  imasaddfnlem  15385  imasaddvallem  15386  imasvscafn  15394  imasvscaval  15395  mreexexlem4d  15504  mreexfidimd  15507  sscpwex  15671  acsmap2d  16376  gsumress  16470  subsubm  16555  frmdsssubm  16596  frmdss2  16598  subsubg  16791  cntzmhm2  16944  cntzcmnf  17418  ablcntzd  17430  gsumzsubmcl  17486  gsumconst  17502  gsumzmhm  17505  gsumzoppg  17512  subgdmdprd  17602  dprdcntz2  17606  dprd2da  17610  dmdprdsplit2lem  17613  ablfac1eu  17641  pgpfaclem1  17649  pgpfaclem2  17650  issubdrg  17968  subsubrg  17969  lmhmlsp  18207  lspsntri  18255  lspindpi  18290  lidldvgen  18414  opsrtoslem2  18643  gsumfsum  18969  mrccss  19188  frlmsslsp  19285  scmatsgrp1  19478  toponss  19875  ssntr  20004  elcls3  20030  toponmre  20040  neiptoptop  20078  neiptopnei  20079  neitr  20127  ordtbas  20139  ordtopn1  20141  ordtopn2  20142  iscnp3  20191  tgcn  20199  tgcnp  20200  ssidcn  20202  cnclsi  20219  cncls  20221  cncnp  20227  lmcld  20250  tgcmp  20347  cnconn  20368  conima  20371  clscon  20376  concompcld  20380  1stccnp  20408  kgentopon  20484  llycmpkgen2  20496  1stckgen  20500  kgencn2  20503  ptopn  20529  txcls  20550  ptpjcn  20557  ptclsg  20561  xkoccn  20565  txcnp  20566  ptcnplem  20567  txcmplem2  20588  xkoptsub  20600  xkopt  20601  xkoco2cn  20604  xkococnlem  20605  xkoinjcn  20633  imasnopn  20636  imasncld  20637  imasncls  20638  qtopkgen  20656  basqtop  20657  tgqtop  20658  qtoprest  20663  kqsat  20677  kqcldsat  20679  kqnrmlem1  20689  kqnrmlem2  20690  hmeontr  20715  reghmph  20739  nrmhmph  20740  fmfnfmlem4  20903  fmfnfm  20904  flimopn  20921  flimclslem  20930  flfnei  20937  lmflf  20951  txflf  20952  fclsopn  20960  fclsfnflim  20973  alexsublem  20990  ptcmplem3  21000  cnextcn  21013  symgtgp  21047  submtmd  21050  subgtgp  21051  clssubg  21054  clsnsg  21055  tgpconcompeqg  21057  snclseqg  21061  tsmscls  21083  trust  21175  restutop  21183  restutopopn  21184  utop3cls  21197  utopreg  21198  trcfilu  21240  blssec  21381  prdsbl  21437  blssopn  21441  metcnp  21487  cfilucfil  21505  psmetutop  21513  iccntr  21750  icccmplem2  21752  reconnlem1  21755  metnrmlem1a  21786  metnrmlem1  21787  metnrmlem2  21788  metnrmlem3  21789  cnheibor  21879  lebnumlem1  21885  lebnumlem3  21887  lebnumii  21890  clsocv  22114  iscfil2  22129  iscmet3  22156  cmetss  22177  relcmpcmet  22179  bcthlem5  22189  itg1addlem5  22535  perfdvf  22735  dvres3  22745  dvres3a  22746  dvcmul  22775  dvcmulf  22776  dvlip2  22824  lhop1lem  22842  dvcnvrelem1  22846  dvcnvrelem2  22847  dvcnvre  22848  dvcvx  22849  plyco0  23014  plyaddlem1  23035  plymullem1  23036  aalioulem3  23155  ulmdvlem1  23220  axcontlem10  24849  eengtrkg  24861  eupares  25548  ghsubgolemOLD  25943  hsupunss  26831  pjpjpre  26907  ssmd2  27800  superpos  27842  atexch  27869  curry2ima  28129  madjusmdetlem2  28493  ordtconlem1  28569  measiuns  28878  imambfm  28923  cnmbfm  28924  dya2iocnrect  28942  omsfval  28955  omssubaddlem  28960  omssubadd  28961  totprobd  29085  fzssfzo  29210  signstfvn  29246  bnj999  29556  bnj1408  29633  bnj1442  29646  bnj1450  29647  bnj1501  29664  cvmsss2  29785  cvmliftmolem1  29792  cvmliftlem3  29798  cvmlift2lem9  29822  cvmlift2lem11  29824  cvmlift3lem6  29835  cvmlift3lem7  29836  ssmclslem  29991  mclsax  29995  mclsppslem  30009  mclspps  30010  dfrdg2  30229  trpredtr  30258  neiin  30773  neibastop2  30802  filnetlem4  30822  poimirlem11  31654  poimirlem12  31655  itg2addnclem2  31697  cnres2  31798  sstotbnd2  31809  sstotbnd  31810  prdstotbnd  31829  heibor1lem  31844  igenval2  32002  lshpnelb  32258  lcvexchlem4  32311  lsatexch  32317  l1cvat  32329  lkrscss  32372  lkrss  32442  lkreqN  32444  paddunN  33200  osumcllem2N  33230  pmapojoinN  33241  pl42lem2N  33253  dibglbN  34442  diblss  34446  dicvaddcl  34466  dicvscacl  34467  diclss  34469  cdlemn5pre  34476  dihord5apre  34538  dihglblem3N  34571  dihglb2  34618  dochsat  34659  dochshpncl  34660  djhspss  34682  dihsumssj  34684  mapdlsm  34940  hdmaprnlem3eN  35137  hdmaplkr  35192  fnwe2lem2  35614  lnmlsslnm  35644  lmhmfgima  35647  hbtlem6  35693  trrelsuperreldg  35898  iunrelexpuztr  35949  funfvima2d  36248  dvsconst  36315  dvsinax  37354  dvbdfbdioolem1  37371  itgsinexplem1  37398  itgperiod  37426  stoweidlem39  37468  dirkeritg  37532  fourierdlem48  37585  fourierdlem49  37586  fourierdlem70  37607  fourierdlem71  37608  fourierdlem81  37618  pfxccatin12  38355  subsubmgm  38554  rmsuppss  38914
  Copyright terms: Public domain W3C validator