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

Theorem sseqtrd 3227
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 3219 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 201 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:  sseqtr4d  3228  uniintsn  3915  oeeui  6616  nnaword2  6644  oaabs2  6659  erssxp  6699  fipwuni  7195  ordtypelem7  7255  cantnflem3  7409  cdainf  7834  ficardun2  7845  ackbij1lem12  7873  ackbij1b  7881  fin1a2lem13  8054  winafp  8335  ioodisj  10781  vdwlem11  13054  mrcssv  13532  mrcsscl  13538  mrcuni  13539  mressmrcd  13545  mreexexlem2d  13563  mreexexlem3d  13564  mreexfidimd  13568  subcss2  13733  resssetc  13940  funcsetcres2  13941  poslubdg  14268  ipodrsfi  14282  acsmap2d  14298  mrelatlub  14305  mreclat  14306  subsubm  14450  subsubg  14656  oppglsm  14969  subglsm  14998  lsmdisj  15006  gsumval3  15207  dprdres  15279  dprdss  15280  dprd2da  15293  dmdprdsplit2lem  15296  ablfac1b  15321  pgpfac1lem3  15328  issubdrg  15586  subsubrg  15587  islssd  15709  lspun  15760  lspssp  15761  lsslsp  15788  lsmssspx  15857  lspabs2  15889  lspabs3  15890  lspsolvlem  15911  lbsextlem3  15929  mplbas2  16228  qsssubdrg  16447  obselocv  16644  tgcl  16723  basgen  16742  tgfiss  16745  bastop1  16747  bastop2  16748  clsss2  16825  elcls3  16836  topssnei  16877  restcls  16927  restlp  16929  ordtrest2  16950  iscncl  17014  cncls2  17018  cncls  17019  cnntr  17020  lmcls  17046  tgcmp  17144  cmpcld  17145  uncmp  17146  hauscmplem  17149  cmpfi  17151  clscon  17172  2ndcsb  17191  2ndcctbss  17197  2ndcomap  17200  nllyrest  17228  1stckgenlem  17264  kgencn2  17268  kgen2cn  17270  ptbasfi  17292  txcld  17314  txcls  17315  txbasval  17317  ptcld  17323  ptclsg  17325  txnlly  17347  hausdiag  17355  txkgen  17362  xkopt  17365  xkopjcn  17366  xkococnlem  17369  cnmpt1res  17386  cnmpt2res  17387  qtopcld  17420  qtoprest  17424  qtopcmap  17426  kqcldsat  17440  kqreglem2  17449  kqnrmlem2  17451  hmeontr  17476  neifil  17591  fgtr  17601  trnei  17603  uffixfr  17634  uffix2  17635  uffixsn  17636  elflim  17682  flimclslem  17695  fclsopn  17725  fclscmpi  17740  fclscmp  17741  alexsubALTlem3  17759  alexsubALT  17761  ptcmplem3  17764  subgntr  17805  opnsubg  17806  clssubg  17807  clsnsg  17808  cldsubg  17809  tgpconcompeqg  17810  snclseqg  17814  tsmsgsum  17837  tsmsid  17838  tgptsmscld  17849  ressprdsds  17951  lpbl  18065  met2ndci  18084  prdsxmslem2  18091  tgioo  18318  metdstri  18371  metdseq0  18374  xlebnum  18479  clsocv  18693  metelcls  18746  cmetss  18756  relcmpcmet  18758  cmpcmet  18759  minveclem4a  18810  uniioovol  18950  uniioombllem3  18956  limcres  19252  dvbss  19267  perfdvf  19269  dvreslem  19275  dvres2lem  19276  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvcmulf  19310  dvcj  19315  dvnfre  19317  dvmptres2  19327  dvmptcmul  19329  dvmptntr  19336  dvlip2  19358  dvcnvrelem2  19381  ftc1cn  19406  taylfvallem1  19752  taylply2  19763  taylply  19764  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  pserulm  19814  shsub2  21920  spanssoc  21944  shub2  21978  ococin  22003  ssjo  22042  chub2  22103  spanpr  22175  elnlfn  22524  mdslj1i  22915  mdslmd3i  22928  mdexchi  22931  chirredlem1  22986  atcvat3i  22992  mdsymlem1  22999  mdsymlem5  23003  esumpfinvallem  23457  cvmscld  23819  cvmliftmolem1  23827  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift3lem6  23870  nodense  24414  ftc1cnnc  25025  prdnei  25676  dualalg  25885  opnregcld  26351  ivthALT  26361  neibastop2  26413  fnemeet1  26418  fnejoin1  26420  sstotbnd  26602  ssbnd  26615  heibor1lem  26636  heiborlem3  26640  heibor  26648  ismrcd1  26876  ismrcd2  26877  coeq0i  26935  lsslindf  27403  hbtlem6  27436  rgspnval  27476  stoweidlem34  27886  lsmsat  29820  lssats  29824  lcvexchlem3  29848  lsatcvat3  29864  lkrscss  29910  lkrpssN  29975  pmod1i  30659  pclbtwnN  30708  pclunN  30709  pclss2polN  30732  pcl0N  30733  sspmaplubN  30736  paddunN  30738  pnonsingN  30744  pclfinclN  30761  osumcllem4N  30770  dia2dimlem13  31888  dvhopellsm  31929  dvadiaN  31940  dicelval1stN  32000  dicelval2nd  32001  dihssxp  32064  dihvalrel  32091  dochsscl  32180  dihoml4  32189  dochnoncon  32203  dvh3dim3N  32261  lcfrlem2  32355  lcfrlem5  32358  lcfr  32397  lcdlsp  32433  mapdsn  32453  mapdlsm  32476  mapdpglem1  32484  mapdindp0  32531  hlhilocv  32772
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