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

Theorem sseqtrd 3380
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 3372 . 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 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sseqtr4d  3381  uniintsn  4153  oeeui  7029  nnaword2  7057  oaabs2  7072  erssxp  7112  fipwuni  7664  ordtypelem7  7726  cantnflem3  7887  cantnflem3OLD  7909  cdainf  8349  ficardun2  8360  ackbij1lem12  8388  ackbij1b  8396  fin1a2lem13  8569  winafp  8852  ioodisj  11402  vdwlem11  14035  mrcssv  14535  mrcsscl  14541  mrcuni  14542  mressmrcd  14548  mreexexlem2d  14566  mreexexlem3d  14567  mreexfidimd  14571  subcss2  14736  resssetc  14943  funcsetcres2  14944  poslubdg  15302  ipodrsfi  15316  acsmap2d  15332  mrelatlub  15339  mreclatBAD  15340  subsubm  15467  subsubg  15684  oppglsm  16121  subglsm  16150  lsmdisj  16158  gsumval3OLD  16362  gsumval3  16365  dprdres  16499  dprdss  16500  dprd2da  16515  dmdprdsplit2lem  16518  ablfac1b  16545  pgpfac1lem3  16552  issubdrg  16814  subsubrg  16815  islssd  16939  lspun  16990  lspssp  16991  lsslsp  17018  lsmssspx  17091  lspabs2  17123  lspabs3  17124  lspsolvlem  17145  lbsextlem3  17163  mplbas2  17483  mplbas2OLD  17484  qsssubdrg  17716  obselocv  17995  lsslindf  18101  tgcl  18416  basgen  18435  tgfiss  18438  bastop1  18440  bastop2  18441  clsss2  18518  elcls3  18529  topssnei  18570  neiptopnei  18578  neitr  18626  restcls  18627  restlp  18629  ordtrest2  18650  iscncl  18715  cncls2  18719  cncls  18720  cnntr  18721  lmcls  18748  tgcmp  18846  cmpcld  18847  uncmp  18848  hauscmplem  18851  cmpfi  18853  clscon  18876  2ndcsb  18895  2ndcctbss  18901  2ndcomap  18904  nllyrest  18932  1stckgenlem  18968  kgencn2  18972  kgen2cn  18974  ptbasfi  18996  txcld  19018  txcls  19019  txbasval  19021  neitx  19022  ptcld  19028  ptclsg  19030  txnlly  19052  hausdiag  19060  txkgen  19067  xkopt  19070  xkopjcn  19071  xkococnlem  19074  cnmpt1res  19091  cnmpt2res  19092  imasnopn  19105  imasncld  19106  imasncls  19107  qtopcld  19128  qtoprest  19132  qtopcmap  19134  kqcldsat  19148  kqreglem2  19157  kqnrmlem2  19159  hmeontr  19184  neifil  19295  fgtr  19305  trnei  19307  uffixfr  19338  uffix2  19339  uffixsn  19340  elflim  19386  flimclslem  19399  fclsopn  19429  fclscmpi  19444  fclscmp  19445  alexsubALTlem3  19463  alexsubALT  19465  ptcmplem3  19468  subgntr  19519  opnsubg  19520  clssubg  19521  clsnsg  19522  cldsubg  19523  tgpconcompeqg  19524  snclseqg  19528  tsmsgsum  19551  tsmsid  19552  tsmsgsumOLD  19554  tsmsidOLD  19555  tgptsmscld  19567  ustssco  19631  utop2nei  19667  utop3cls  19668  utopreg  19669  cnextucn  19720  ressprdsds  19788  lpbl  19920  met2ndci  19939  prdsxmslem2  19946  metustexhalfOLD  19980  metustexhalf  19981  metutopOLD  19999  psmetutop  20000  tgioo  20215  metdstri  20269  metdseq0  20272  xlebnum  20379  clsocv  20604  metelcls  20657  cmetss  20667  relcmpcmet  20669  cmpcmet  20670  minveclem4a  20759  uniioovol  20901  uniioombllem3  20907  limcres  21203  dvbss  21218  perfdvf  21220  dvreslem  21226  dvres2lem  21227  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvcmulf  21261  dvcj  21266  dvnfre  21268  dvmptres2  21278  dvmptcmul  21280  dvmptntr  21287  dvlip2  21309  dvcnvrelem2  21332  ftc1cn  21357  taylfvallem1  21707  taylply2  21718  taylply  21719  dvtaylp  21720  dvntaylp  21721  dvntaylp0  21722  taylthlem1  21723  taylthlem2  21724  ulmdvlem3  21752  pserulm  21772  shsub2  24551  spanssoc  24575  shub2  24609  ococin  24634  ssjo  24673  chub2  24734  spanpr  24806  elnlfn  25155  mdslj1i  25546  mdslmd3i  25559  mdexchi  25562  chirredlem1  25617  atcvat3i  25623  mdsymlem1  25630  mdsymlem5  25634  imadifxp  25763  fsumcvg4  26234  sitgclg  26576  eulerpartlemgf  26610  cvmscld  27010  cvmliftmolem1  27018  cvmlift2lem9  27048  cvmlift2lem11  27050  cvmlift3lem6  27061  prodss  27307  nodense  27677  ftc1cnnc  28310  opnregcld  28369  ivthALT  28374  neibastop2  28426  fnemeet1  28431  fnejoin1  28433  sstotbnd  28518  ssbnd  28531  heibor1lem  28552  heiborlem3  28556  heibor  28564  ismrcd1  28879  ismrcd2  28880  coeq0i  28936  hbtlem6  29330  rgspnval  29370  iocinico  29432  lsmsat  32226  lssats  32230  lcvexchlem3  32254  lsatcvat3  32270  lkrscss  32316  lkrpssN  32381  pmod1i  33065  pclbtwnN  33114  pclunN  33115  pclss2polN  33138  pcl0N  33139  sspmaplubN  33142  paddunN  33144  pnonsingN  33150  pclfinclN  33167  osumcllem4N  33176  dia2dimlem13  34294  dvhopellsm  34335  dvadiaN  34346  dicelval1stN  34406  dicelval2nd  34407  dihssxp  34470  dihvalrel  34497  dochsscl  34586  dihoml4  34595  dochnoncon  34609  dvh3dim3N  34667  lcfrlem2  34761  lcfrlem5  34764  lcfr  34803  lcdlsp  34839  mapdsn  34859  mapdlsm  34882  mapdpglem1  34890  mapdindp0  34937  hlhilocv  35178
  Copyright terms: Public domain W3C validator