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

Theorem sseqtrd 3327
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 3319 . 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 3263
This theorem is referenced by:  sseqtr4d  3328  uniintsn  4029  oeeui  6781  nnaword2  6809  oaabs2  6824  erssxp  6864  fipwuni  7366  ordtypelem7  7426  cantnflem3  7580  cdainf  8005  ficardun2  8016  ackbij1lem12  8044  ackbij1b  8052  fin1a2lem13  8225  winafp  8505  ioodisj  10958  vdwlem11  13286  mrcssv  13766  mrcsscl  13772  mrcuni  13773  mressmrcd  13779  mreexexlem2d  13797  mreexexlem3d  13798  mreexfidimd  13802  subcss2  13967  resssetc  14174  funcsetcres2  14175  poslubdg  14502  ipodrsfi  14516  acsmap2d  14532  mrelatlub  14539  mreclat  14540  subsubm  14684  subsubg  14890  oppglsm  15203  subglsm  15232  lsmdisj  15240  gsumval3  15441  dprdres  15513  dprdss  15514  dprd2da  15527  dmdprdsplit2lem  15530  ablfac1b  15555  pgpfac1lem3  15562  issubdrg  15820  subsubrg  15821  islssd  15939  lspun  15990  lspssp  15991  lsslsp  16018  lsmssspx  16087  lspabs2  16119  lspabs3  16120  lspsolvlem  16141  lbsextlem3  16159  mplbas2  16458  qsssubdrg  16681  obselocv  16878  tgcl  16957  basgen  16976  tgfiss  16979  bastop1  16981  bastop2  16982  clsss2  17059  elcls3  17070  topssnei  17111  neiptopnei  17119  neitr  17166  restcls  17167  restlp  17169  ordtrest2  17190  iscncl  17255  cncls2  17259  cncls  17260  cnntr  17261  lmcls  17288  tgcmp  17386  cmpcld  17387  uncmp  17388  hauscmplem  17391  cmpfi  17393  clscon  17414  2ndcsb  17433  2ndcctbss  17439  2ndcomap  17442  nllyrest  17470  1stckgenlem  17506  kgencn2  17510  kgen2cn  17512  ptbasfi  17534  txcld  17556  txcls  17557  txbasval  17559  neitx  17560  ptcld  17566  ptclsg  17568  txnlly  17590  hausdiag  17598  txkgen  17605  xkopt  17608  xkopjcn  17609  xkococnlem  17612  cnmpt1res  17629  cnmpt2res  17630  imasnopn  17643  imasncld  17644  imasncls  17645  qtopcld  17666  qtoprest  17670  qtopcmap  17672  kqcldsat  17686  kqreglem2  17695  kqnrmlem2  17697  hmeontr  17722  neifil  17833  fgtr  17843  trnei  17845  uffixfr  17876  uffix2  17877  uffixsn  17878  elflim  17924  flimclslem  17937  fclsopn  17967  fclscmpi  17982  fclscmp  17983  alexsubALTlem3  18001  alexsubALT  18003  ptcmplem3  18006  subgntr  18057  opnsubg  18058  clssubg  18059  clsnsg  18060  cldsubg  18061  tgpconcompeqg  18062  snclseqg  18066  tsmsgsum  18089  tsmsid  18090  tgptsmscld  18101  ustssco  18165  utop2nei  18201  utop3cls  18202  utopreg  18203  cnextucn  18254  ressprdsds  18309  lpbl  18423  met2ndci  18442  prdsxmslem2  18449  metustexhalf  18476  metutop  18487  tgioo  18698  metdstri  18752  metdseq0  18755  xlebnum  18861  clsocv  19075  metelcls  19128  cmetss  19138  relcmpcmet  19140  cmpcmet  19141  minveclem4a  19198  uniioovol  19338  uniioombllem3  19344  limcres  19640  dvbss  19655  perfdvf  19657  dvreslem  19663  dvres2lem  19664  dvcnp2  19673  dvaddbr  19691  dvmulbr  19692  dvcmulf  19698  dvcj  19703  dvnfre  19705  dvmptres2  19715  dvmptcmul  19717  dvmptntr  19724  dvlip2  19746  dvcnvrelem2  19769  ftc1cn  19794  taylfvallem1  20140  taylply2  20151  taylply  20152  dvtaylp  20153  dvntaylp  20154  dvntaylp0  20155  taylthlem1  20156  taylthlem2  20157  ulmdvlem3  20185  pserulm  20205  shsub2  22675  spanssoc  22699  shub2  22733  ococin  22758  ssjo  22797  chub2  22858  spanpr  22930  elnlfn  23279  mdslj1i  23670  mdslmd3i  23683  mdexchi  23686  chirredlem1  23741  atcvat3i  23747  mdsymlem1  23754  mdsymlem5  23758  imadifxp  23881  cvmscld  24739  cvmliftmolem1  24747  cvmlift2lem9  24777  cvmlift2lem11  24779  cvmlift3lem6  24790  prodss  25052  nodense  25367  ftc1cnnc  25979  opnregcld  26024  ivthALT  26029  neibastop2  26081  fnemeet1  26086  fnejoin1  26088  sstotbnd  26175  ssbnd  26188  heibor1lem  26209  heiborlem3  26213  heibor  26221  ismrcd1  26443  ismrcd2  26444  coeq0i  26502  lsslindf  26969  hbtlem6  27002  rgspnval  27042  lsmsat  29123  lssats  29127  lcvexchlem3  29151  lsatcvat3  29167  lkrscss  29213  lkrpssN  29278  pmod1i  29962  pclbtwnN  30011  pclunN  30012  pclss2polN  30035  pcl0N  30036  sspmaplubN  30039  paddunN  30041  pnonsingN  30047  pclfinclN  30064  osumcllem4N  30073  dia2dimlem13  31191  dvhopellsm  31232  dvadiaN  31243  dicelval1stN  31303  dicelval2nd  31304  dihssxp  31367  dihvalrel  31394  dochsscl  31483  dihoml4  31492  dochnoncon  31506  dvh3dim3N  31564  lcfrlem2  31658  lcfrlem5  31661  lcfr  31700  lcdlsp  31736  mapdsn  31756  mapdlsm  31779  mapdpglem1  31787  mapdindp0  31834  hlhilocv  32075
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 2368
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 2374  df-cleq 2380  df-clel 2383  df-in 3270  df-ss 3277
  Copyright terms: Public domain W3C validator