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

Theorem sseqtrd 3344
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 3336 . 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 3280
This theorem is referenced by:  sseqtr4d  3345  uniintsn  4047  oeeui  6804  nnaword2  6832  oaabs2  6847  erssxp  6887  fipwuni  7389  ordtypelem7  7449  cantnflem3  7603  cdainf  8028  ficardun2  8039  ackbij1lem12  8067  ackbij1b  8075  fin1a2lem13  8248  winafp  8528  ioodisj  10982  vdwlem11  13314  mrcssv  13794  mrcsscl  13800  mrcuni  13801  mressmrcd  13807  mreexexlem2d  13825  mreexexlem3d  13826  mreexfidimd  13830  subcss2  13995  resssetc  14202  funcsetcres2  14203  poslubdg  14530  ipodrsfi  14544  acsmap2d  14560  mrelatlub  14567  mreclat  14568  subsubm  14712  subsubg  14918  oppglsm  15231  subglsm  15260  lsmdisj  15268  gsumval3  15469  dprdres  15541  dprdss  15542  dprd2da  15555  dmdprdsplit2lem  15558  ablfac1b  15583  pgpfac1lem3  15590  issubdrg  15848  subsubrg  15849  islssd  15967  lspun  16018  lspssp  16019  lsslsp  16046  lsmssspx  16115  lspabs2  16147  lspabs3  16148  lspsolvlem  16169  lbsextlem3  16187  mplbas2  16486  qsssubdrg  16713  obselocv  16910  tgcl  16989  basgen  17008  tgfiss  17011  bastop1  17013  bastop2  17014  clsss2  17091  elcls3  17102  topssnei  17143  neiptopnei  17151  neitr  17198  restcls  17199  restlp  17201  ordtrest2  17222  iscncl  17287  cncls2  17291  cncls  17292  cnntr  17293  lmcls  17320  tgcmp  17418  cmpcld  17419  uncmp  17420  hauscmplem  17423  cmpfi  17425  clscon  17446  2ndcsb  17465  2ndcctbss  17471  2ndcomap  17474  nllyrest  17502  1stckgenlem  17538  kgencn2  17542  kgen2cn  17544  ptbasfi  17566  txcld  17588  txcls  17589  txbasval  17591  neitx  17592  ptcld  17598  ptclsg  17600  txnlly  17622  hausdiag  17630  txkgen  17637  xkopt  17640  xkopjcn  17641  xkococnlem  17644  cnmpt1res  17661  cnmpt2res  17662  imasnopn  17675  imasncld  17676  imasncls  17677  qtopcld  17698  qtoprest  17702  qtopcmap  17704  kqcldsat  17718  kqreglem2  17727  kqnrmlem2  17729  hmeontr  17754  neifil  17865  fgtr  17875  trnei  17877  uffixfr  17908  uffix2  17909  uffixsn  17910  elflim  17956  flimclslem  17969  fclsopn  17999  fclscmpi  18014  fclscmp  18015  alexsubALTlem3  18033  alexsubALT  18035  ptcmplem3  18038  subgntr  18089  opnsubg  18090  clssubg  18091  clsnsg  18092  cldsubg  18093  tgpconcompeqg  18094  snclseqg  18098  tsmsgsum  18121  tsmsid  18122  tgptsmscld  18133  ustssco  18197  utop2nei  18233  utop3cls  18234  utopreg  18235  cnextucn  18286  ressprdsds  18354  lpbl  18486  met2ndci  18505  prdsxmslem2  18512  metustexhalfOLD  18546  metustexhalf  18547  metutopOLD  18565  psmetutop  18566  tgioo  18780  metdstri  18834  metdseq0  18837  xlebnum  18943  clsocv  19157  metelcls  19210  cmetss  19220  relcmpcmet  19222  cmpcmet  19223  minveclem4a  19284  uniioovol  19424  uniioombllem3  19430  limcres  19726  dvbss  19741  perfdvf  19743  dvreslem  19749  dvres2lem  19750  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcmulf  19784  dvcj  19789  dvnfre  19791  dvmptres2  19801  dvmptcmul  19803  dvmptntr  19810  dvlip2  19832  dvcnvrelem2  19855  ftc1cn  19880  taylfvallem1  20226  taylply2  20237  taylply  20238  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulmdvlem3  20271  pserulm  20291  shsub2  22780  spanssoc  22804  shub2  22838  ococin  22863  ssjo  22902  chub2  22963  spanpr  23035  elnlfn  23384  mdslj1i  23775  mdslmd3i  23788  mdexchi  23791  chirredlem1  23846  atcvat3i  23852  mdsymlem1  23859  mdsymlem5  23863  imadifxp  23991  sitgclg  24609  cvmscld  24913  cvmliftmolem1  24921  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift3lem6  24964  prodss  25226  nodense  25557  ftc1cnnc  26178  opnregcld  26223  ivthALT  26228  neibastop2  26280  fnemeet1  26285  fnejoin1  26287  sstotbnd  26374  ssbnd  26387  heibor1lem  26408  heiborlem3  26412  heibor  26420  ismrcd1  26642  ismrcd2  26643  coeq0i  26701  lsslindf  27168  hbtlem6  27201  rgspnval  27241  lsmsat  29491  lssats  29495  lcvexchlem3  29519  lsatcvat3  29535  lkrscss  29581  lkrpssN  29646  pmod1i  30330  pclbtwnN  30379  pclunN  30380  pclss2polN  30403  pcl0N  30404  sspmaplubN  30407  paddunN  30409  pnonsingN  30415  pclfinclN  30432  osumcllem4N  30441  dia2dimlem13  31559  dvhopellsm  31600  dvadiaN  31611  dicelval1stN  31671  dicelval2nd  31672  dihssxp  31735  dihvalrel  31762  dochsscl  31851  dihoml4  31860  dochnoncon  31874  dvh3dim3N  31932  lcfrlem2  32026  lcfrlem5  32029  lcfr  32068  lcdlsp  32104  mapdsn  32124  mapdlsm  32147  mapdpglem1  32155  mapdindp0  32202  hlhilocv  32443
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator