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

Theorem sseqtrd 3525
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrd.1  |-  ( ph  ->  A  C_  B )
sseqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
sseqtrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32sseq2d 3517 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 210 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  sseqtr4d  3526  uniintsn  4309  oeeui  7253  nnaword2  7281  oaabs2  7296  erssxp  7336  fipwuni  7888  ordtypelem7  7952  cantnflem3  8113  cantnflem3OLD  8135  cdainf  8575  ficardun2  8586  ackbij1lem12  8614  ackbij1b  8622  fin1a2lem13  8795  winafp  9078  ioodisj  11661  prodss  13736  vdwlem11  14491  mrcssv  14993  mrcsscl  14999  mrcuni  15000  mressmrcd  15006  mreexexlem2d  15024  mreexexlem3d  15025  mreexfidimd  15029  subcss2  15191  resssetc  15398  funcsetcres2  15399  poslubdg  15758  ipodrsfi  15772  acsmap2d  15788  mrelatlub  15795  mreclatBAD  15796  subsubm  15967  subsubg  16203  oppglsm  16641  subglsm  16670  lsmdisj  16678  gsumval3OLD  16887  gsumval3  16890  dprdres  17054  dprdss  17055  dprd2da  17070  dmdprdsplit2lem  17073  ablfac1b  17100  pgpfac1lem3  17107  issubdrg  17433  subsubrg  17434  islssd  17561  lspun  17612  lspssp  17613  lsslsp  17640  lsmssspx  17713  lspabs2  17745  lspabs3  17746  lspsolvlem  17767  lbsextlem3  17785  mplbas2  18113  mplbas2OLD  18114  gsumply1subr  18254  qsssubdrg  18456  obselocv  18737  lsslindf  18843  tgcl  19449  basgen  19468  tgfiss  19471  bastop1  19473  bastop2  19474  clsss2  19551  elcls3  19562  topssnei  19603  neiptopnei  19611  neitr  19659  restcls  19660  restlp  19662  ordtrest2  19683  iscncl  19748  cncls2  19752  cncls  19753  cnntr  19754  lmcls  19781  tgcmp  19879  cmpcld  19880  uncmp  19881  hauscmplem  19884  cmpfi  19886  clscon  19909  2ndcsb  19928  2ndcctbss  19934  2ndcomap  19937  nllyrest  19965  1stckgenlem  20032  kgencn2  20036  kgen2cn  20038  ptbasfi  20060  txcld  20082  txcls  20083  txbasval  20085  neitx  20086  ptcld  20092  ptclsg  20094  txnlly  20116  hausdiag  20124  txkgen  20131  xkopt  20134  xkopjcn  20135  xkococnlem  20138  cnmpt1res  20155  cnmpt2res  20156  imasnopn  20169  imasncld  20170  imasncls  20171  qtopcld  20192  qtoprest  20196  qtopcmap  20198  kqcldsat  20212  kqreglem2  20221  kqnrmlem2  20223  hmeontr  20248  neifil  20359  fgtr  20369  trnei  20371  uffixfr  20402  uffix2  20403  uffixsn  20404  elflim  20450  flimclslem  20463  fclsopn  20493  fclscmpi  20508  fclscmp  20509  alexsubALTlem3  20527  alexsubALT  20529  ptcmplem3  20532  subgntr  20583  opnsubg  20584  clssubg  20585  clsnsg  20586  cldsubg  20587  tgpconcompeqg  20588  snclseqg  20592  tsmsgsum  20615  tsmsid  20616  tsmsgsumOLD  20618  tsmsidOLD  20619  tgptsmscld  20631  ustssco  20695  utop2nei  20731  utop3cls  20732  utopreg  20733  cnextucn  20784  ressprdsds  20852  lpbl  20984  met2ndci  21003  prdsxmslem2  21010  metustexhalfOLD  21044  metustexhalf  21045  metutopOLD  21063  psmetutop  21064  tgioo  21279  metdstri  21333  metdseq0  21336  xlebnum  21443  clsocv  21668  metelcls  21721  cmetss  21731  relcmpcmet  21733  cmpcmet  21734  minveclem4a  21823  uniioovol  21966  uniioombllem3  21972  limcres  22268  dvbss  22283  perfdvf  22285  dvreslem  22291  dvres2lem  22292  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcmulf  22326  dvcj  22331  dvnfre  22333  dvmptres2  22343  dvmptcmul  22345  dvmptntr  22352  dvlip2  22374  dvcnvrelem2  22397  ftc1cn  22422  taylfvallem1  22730  taylply2  22741  taylply  22742  dvtaylp  22743  dvntaylp  22744  dvntaylp0  22745  taylthlem1  22746  taylthlem2  22747  ulmdvlem3  22775  pserulm  22795  shsub2  26221  spanssoc  26245  shub2  26279  ococin  26304  ssjo  26343  chub2  26404  spanpr  26476  elnlfn  26825  mdslj1i  27216  mdslmd3i  27229  mdexchi  27232  chirredlem1  27287  atcvat3i  27293  mdsymlem1  27300  mdsymlem5  27304  imadifxp  27436  qtophaus  27817  locfinreflem  27821  fsumcvg4  27910  omsfval  28243  omsmon  28245  sitgclg  28262  eulerpartlemgf  28296  cvmscld  28696  cvmliftmolem1  28704  cvmlift2lem9  28734  cvmlift2lem11  28736  cvmlift3lem6  28747  nodense  29425  ftc1cnnc  30065  opnregcld  30124  ivthALT  30129  neibastop2  30155  fnemeet1  30160  fnejoin1  30162  sstotbnd  30247  ssbnd  30260  heibor1lem  30281  heiborlem3  30285  heibor  30293  ismrcd1  30606  ismrcd2  30607  coeq0i  30662  hbtlem6  31054  rgspnval  31093  iocinico  31155  iccdifprioo  31510  cncfuni  31643  cncfiooicclem1  31650  dvresntr  31667  dvmptresicc  31670  itgsubsticclem  31728  fourierdlem42  31885  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  subsubmgm  32439  estrres  32611  lsmsat  34608  lssats  34612  lcvexchlem3  34636  lsatcvat3  34652  lkrscss  34698  lkrpssN  34763  pmod1i  35447  pclbtwnN  35496  pclunN  35497  pclss2polN  35520  pcl0N  35521  sspmaplubN  35524  paddunN  35526  pnonsingN  35532  pclfinclN  35549  osumcllem4N  35558  dia2dimlem13  36678  dvhopellsm  36719  dvadiaN  36730  dicelval1stN  36790  dicelval2nd  36791  dihssxp  36854  dihvalrel  36881  dochsscl  36970  dihoml4  36979  dochnoncon  36993  dvh3dim3N  37051  lcfrlem2  37145  lcfrlem5  37148  lcfr  37187  lcdlsp  37223  mapdsn  37243  mapdlsm  37266  mapdpglem1  37274  mapdindp0  37321  hlhilocv  37562
  Copyright terms: Public domain W3C validator