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

Theorem sseqtrd 3215
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 3207 . 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 1623    C_ wss 3153
This theorem is referenced by:  sseqtr4d  3216  uniintsn  3900  oeeui  6596  nnaword2  6624  oaabs2  6639  erssxp  6679  fipwuni  7175  ordtypelem7  7235  cantnflem3  7389  cdainf  7814  ficardun2  7825  ackbij1lem12  7853  ackbij1b  7861  fin1a2lem13  8034  winafp  8315  ioodisj  10761  vdwlem11  13034  mrcssv  13512  mrcsscl  13518  mrcuni  13519  mressmrcd  13525  mreexexlem2d  13543  mreexexlem3d  13544  mreexfidimd  13548  subcss2  13713  resssetc  13920  funcsetcres2  13921  poslubdg  14248  ipodrsfi  14262  acsmap2d  14278  mrelatlub  14285  mreclat  14286  subsubm  14430  subsubg  14636  oppglsm  14949  subglsm  14978  lsmdisj  14986  gsumval3  15187  dprdres  15259  dprdss  15260  dprd2da  15273  dmdprdsplit2lem  15276  ablfac1b  15301  pgpfac1lem3  15308  issubdrg  15566  subsubrg  15567  islssd  15689  lspun  15740  lspssp  15741  lsslsp  15768  lsmssspx  15837  lspabs2  15869  lspabs3  15870  lspsolvlem  15891  lbsextlem3  15909  mplbas2  16208  qsssubdrg  16427  obselocv  16624  tgcl  16703  basgen  16722  tgfiss  16725  bastop1  16727  bastop2  16728  clsss2  16805  elcls3  16816  topssnei  16857  restcls  16907  restlp  16909  ordtrest2  16930  iscncl  16994  cncls2  16998  cncls  16999  cnntr  17000  lmcls  17026  tgcmp  17124  cmpcld  17125  uncmp  17126  hauscmplem  17129  cmpfi  17131  clscon  17152  2ndcsb  17171  2ndcctbss  17177  2ndcomap  17180  nllyrest  17208  1stckgenlem  17244  kgencn2  17248  kgen2cn  17250  ptbasfi  17272  txcld  17294  txcls  17295  txbasval  17297  ptcld  17303  ptclsg  17305  txnlly  17327  hausdiag  17335  txkgen  17342  xkopt  17345  xkopjcn  17346  xkococnlem  17349  cnmpt1res  17366  cnmpt2res  17367  qtopcld  17400  qtoprest  17404  qtopcmap  17406  kqcldsat  17420  kqreglem2  17429  kqnrmlem2  17431  hmeontr  17456  neifil  17571  fgtr  17581  trnei  17583  uffixfr  17614  uffix2  17615  uffixsn  17616  elflim  17662  flimclslem  17675  fclsopn  17705  fclscmpi  17720  fclscmp  17721  alexsubALTlem3  17739  alexsubALT  17741  ptcmplem3  17744  subgntr  17785  opnsubg  17786  clssubg  17787  clsnsg  17788  cldsubg  17789  tgpconcompeqg  17790  snclseqg  17794  tsmsgsum  17817  tsmsid  17818  tgptsmscld  17829  ressprdsds  17931  lpbl  18045  met2ndci  18064  prdsxmslem2  18071  tgioo  18298  metdstri  18351  metdseq0  18354  xlebnum  18459  clsocv  18673  metelcls  18726  cmetss  18736  relcmpcmet  18738  cmpcmet  18739  minveclem4a  18790  uniioovol  18930  uniioombllem3  18936  limcres  19232  dvbss  19247  perfdvf  19249  dvreslem  19255  dvres2lem  19256  dvcnp2  19265  dvaddbr  19283  dvmulbr  19284  dvcmulf  19290  dvcj  19295  dvnfre  19297  dvmptres2  19307  dvmptcmul  19309  dvmptntr  19316  dvlip2  19338  dvcnvrelem2  19361  ftc1cn  19386  taylfvallem1  19732  taylply2  19743  taylply  19744  dvtaylp  19745  dvntaylp  19746  dvntaylp0  19747  taylthlem1  19748  taylthlem2  19749  ulmdvlem3  19775  pserulm  19794  shsub2  21900  spanssoc  21924  shub2  21958  ococin  21983  ssjo  22022  chub2  22083  spanpr  22155  elnlfn  22504  mdslj1i  22895  mdslmd3i  22908  mdexchi  22911  chirredlem1  22966  atcvat3i  22972  mdsymlem1  22979  mdsymlem5  22983  cvmscld  23211  cvmliftmolem1  23219  cvmlift2lem9  23249  cvmlift2lem11  23251  cvmlift3lem6  23262  axdense  23747  prdnei  24984  dualalg  25193  opnregcld  25659  ivthALT  25669  neibastop2  25721  fnemeet1  25726  fnejoin1  25728  sstotbnd  25910  ssbnd  25923  heibor1lem  25944  heiborlem3  25948  heibor  25956  ismrcd1  26184  ismrcd2  26185  coeq0i  26243  lsslindf  26711  hbtlem6  26744  rgspnval  26784  stoweidlem34  27194  lsmsat  28477  lssats  28481  lcvexchlem3  28505  lsatcvat3  28521  lkrscss  28567  lkrpssN  28632  pmod1i  29316  pclbtwnN  29365  pclunN  29366  pclss2polN  29389  pcl0N  29390  sspmaplubN  29393  paddunN  29395  pnonsingN  29401  pclfinclN  29418  osumcllem4N  29427  dia2dimlem13  30545  dvhopellsm  30586  dvadiaN  30597  dicelval1stN  30657  dicelval2nd  30658  dihssxp  30721  dihvalrel  30748  dochsscl  30837  dihoml4  30846  dochnoncon  30860  dvh3dim3N  30918  lcfrlem2  31012  lcfrlem5  31015  lcfr  31054  lcdlsp  31090  mapdsn  31110  mapdlsm  31133  mapdpglem1  31141  mapdindp0  31188  hlhilocv  31429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator