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

Theorem sseqtrd 3321
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 3313 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 202 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3257
This theorem is referenced by:  sseqtr4d  3322  uniintsn  4023  oeeui  6775  nnaword2  6803  oaabs2  6818  erssxp  6858  fipwuni  7360  ordtypelem7  7420  cantnflem3  7574  cdainf  7999  ficardun2  8010  ackbij1lem12  8038  ackbij1b  8046  fin1a2lem13  8219  winafp  8499  ioodisj  10952  vdwlem11  13280  mrcssv  13760  mrcsscl  13766  mrcuni  13767  mressmrcd  13773  mreexexlem2d  13791  mreexexlem3d  13792  mreexfidimd  13796  subcss2  13961  resssetc  14168  funcsetcres2  14169  poslubdg  14496  ipodrsfi  14510  acsmap2d  14526  mrelatlub  14533  mreclat  14534  subsubm  14678  subsubg  14884  oppglsm  15197  subglsm  15226  lsmdisj  15234  gsumval3  15435  dprdres  15507  dprdss  15508  dprd2da  15521  dmdprdsplit2lem  15524  ablfac1b  15549  pgpfac1lem3  15556  issubdrg  15814  subsubrg  15815  islssd  15933  lspun  15984  lspssp  15985  lsslsp  16012  lsmssspx  16081  lspabs2  16113  lspabs3  16114  lspsolvlem  16135  lbsextlem3  16153  mplbas2  16452  qsssubdrg  16675  obselocv  16872  tgcl  16951  basgen  16970  tgfiss  16973  bastop1  16975  bastop2  16976  clsss2  17053  elcls3  17064  topssnei  17105  neiptopnei  17113  neitr  17160  restcls  17161  restlp  17163  ordtrest2  17184  iscncl  17249  cncls2  17253  cncls  17254  cnntr  17255  lmcls  17282  tgcmp  17380  cmpcld  17381  uncmp  17382  hauscmplem  17385  cmpfi  17387  clscon  17408  2ndcsb  17427  2ndcctbss  17433  2ndcomap  17436  nllyrest  17464  1stckgenlem  17500  kgencn2  17504  kgen2cn  17506  ptbasfi  17528  txcld  17550  txcls  17551  txbasval  17553  neitx  17554  ptcld  17560  ptclsg  17562  txnlly  17584  hausdiag  17592  txkgen  17599  xkopt  17602  xkopjcn  17603  xkococnlem  17606  cnmpt1res  17623  cnmpt2res  17624  imasnopn  17637  imasncld  17638  imasncls  17639  qtopcld  17660  qtoprest  17664  qtopcmap  17666  kqcldsat  17680  kqreglem2  17689  kqnrmlem2  17691  hmeontr  17716  neifil  17827  fgtr  17837  trnei  17839  uffixfr  17870  uffix2  17871  uffixsn  17872  elflim  17918  flimclslem  17931  fclsopn  17961  fclscmpi  17976  fclscmp  17977  alexsubALTlem3  17995  alexsubALT  17997  ptcmplem3  18000  subgntr  18051  opnsubg  18052  clssubg  18053  clsnsg  18054  cldsubg  18055  tgpconcompeqg  18056  snclseqg  18060  tsmsgsum  18083  tsmsid  18084  tgptsmscld  18095  ustssco  18159  utop2nei  18195  utop3cls  18196  utopreg  18197  cnextucn  18248  ressprdsds  18303  lpbl  18417  met2ndci  18436  prdsxmslem2  18443  metustexhalf  18470  metutop  18481  tgioo  18692  metdstri  18746  metdseq0  18749  xlebnum  18855  clsocv  19069  metelcls  19122  cmetss  19132  relcmpcmet  19134  cmpcmet  19135  minveclem4a  19192  uniioovol  19332  uniioombllem3  19338  limcres  19634  dvbss  19649  perfdvf  19651  dvreslem  19657  dvres2lem  19658  dvcnp2  19667  dvaddbr  19685  dvmulbr  19686  dvcmulf  19692  dvcj  19697  dvnfre  19699  dvmptres2  19709  dvmptcmul  19711  dvmptntr  19718  dvlip2  19740  dvcnvrelem2  19763  ftc1cn  19788  taylfvallem1  20134  taylply2  20145  taylply  20146  dvtaylp  20147  dvntaylp  20148  dvntaylp0  20149  taylthlem1  20150  taylthlem2  20151  ulmdvlem3  20179  pserulm  20199  shsub2  22669  spanssoc  22693  shub2  22727  ococin  22752  ssjo  22791  chub2  22852  spanpr  22924  elnlfn  23273  mdslj1i  23664  mdslmd3i  23677  mdexchi  23680  chirredlem1  23735  atcvat3i  23741  mdsymlem1  23748  mdsymlem5  23752  imadifxp  23875  cvmscld  24733  cvmliftmolem1  24741  cvmlift2lem9  24771  cvmlift2lem11  24773  cvmlift3lem6  24784  prodss  25046  nodense  25361  ftc1cnnc  25973  opnregcld  26018  ivthALT  26023  neibastop2  26075  fnemeet1  26080  fnejoin1  26082  sstotbnd  26169  ssbnd  26182  heibor1lem  26203  heiborlem3  26207  heibor  26215  ismrcd1  26437  ismrcd2  26438  coeq0i  26496  lsslindf  26963  hbtlem6  26996  rgspnval  27036  lsmsat  29175  lssats  29179  lcvexchlem3  29203  lsatcvat3  29219  lkrscss  29265  lkrpssN  29330  pmod1i  30014  pclbtwnN  30063  pclunN  30064  pclss2polN  30087  pcl0N  30088  sspmaplubN  30091  paddunN  30093  pnonsingN  30099  pclfinclN  30116  osumcllem4N  30125  dia2dimlem13  31243  dvhopellsm  31284  dvadiaN  31295  dicelval1stN  31355  dicelval2nd  31356  dihssxp  31419  dihvalrel  31446  dochsscl  31535  dihoml4  31544  dochnoncon  31558  dvh3dim3N  31616  lcfrlem2  31710  lcfrlem5  31713  lcfr  31752  lcdlsp  31788  mapdsn  31808  mapdlsm  31831  mapdpglem1  31839  mapdindp0  31886  hlhilocv  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3264  df-ss 3271
  Copyright terms: Public domain W3C validator