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

Theorem sseqtrd 3386
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 3378 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 203 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3322
This theorem is referenced by:  sseqtr4d  3387  uniintsn  4089  oeeui  6848  nnaword2  6876  oaabs2  6891  erssxp  6931  fipwuni  7434  ordtypelem7  7496  cantnflem3  7650  cdainf  8077  ficardun2  8088  ackbij1lem12  8116  ackbij1b  8124  fin1a2lem13  8297  winafp  8577  ioodisj  11031  vdwlem11  13364  mrcssv  13844  mrcsscl  13850  mrcuni  13851  mressmrcd  13857  mreexexlem2d  13875  mreexexlem3d  13876  mreexfidimd  13880  subcss2  14045  resssetc  14252  funcsetcres2  14253  poslubdg  14580  ipodrsfi  14594  acsmap2d  14610  mrelatlub  14617  mreclat  14618  subsubm  14762  subsubg  14968  oppglsm  15281  subglsm  15310  lsmdisj  15318  gsumval3  15519  dprdres  15591  dprdss  15592  dprd2da  15605  dmdprdsplit2lem  15608  ablfac1b  15633  pgpfac1lem3  15640  issubdrg  15898  subsubrg  15899  islssd  16017  lspun  16068  lspssp  16069  lsslsp  16096  lsmssspx  16165  lspabs2  16197  lspabs3  16198  lspsolvlem  16219  lbsextlem3  16237  mplbas2  16536  qsssubdrg  16763  obselocv  16960  tgcl  17039  basgen  17058  tgfiss  17061  bastop1  17063  bastop2  17064  clsss2  17141  elcls3  17152  topssnei  17193  neiptopnei  17201  neitr  17249  restcls  17250  restlp  17252  ordtrest2  17273  iscncl  17338  cncls2  17342  cncls  17343  cnntr  17344  lmcls  17371  tgcmp  17469  cmpcld  17470  uncmp  17471  hauscmplem  17474  cmpfi  17476  clscon  17498  2ndcsb  17517  2ndcctbss  17523  2ndcomap  17526  nllyrest  17554  1stckgenlem  17590  kgencn2  17594  kgen2cn  17596  ptbasfi  17618  txcld  17640  txcls  17641  txbasval  17643  neitx  17644  ptcld  17650  ptclsg  17652  txnlly  17674  hausdiag  17682  txkgen  17689  xkopt  17692  xkopjcn  17693  xkococnlem  17696  cnmpt1res  17713  cnmpt2res  17714  imasnopn  17727  imasncld  17728  imasncls  17729  qtopcld  17750  qtoprest  17754  qtopcmap  17756  kqcldsat  17770  kqreglem2  17779  kqnrmlem2  17781  hmeontr  17806  neifil  17917  fgtr  17927  trnei  17929  uffixfr  17960  uffix2  17961  uffixsn  17962  elflim  18008  flimclslem  18021  fclsopn  18051  fclscmpi  18066  fclscmp  18067  alexsubALTlem3  18085  alexsubALT  18087  ptcmplem3  18090  subgntr  18141  opnsubg  18142  clssubg  18143  clsnsg  18144  cldsubg  18145  tgpconcompeqg  18146  snclseqg  18150  tsmsgsum  18173  tsmsid  18174  tgptsmscld  18185  ustssco  18249  utop2nei  18285  utop3cls  18286  utopreg  18287  cnextucn  18338  ressprdsds  18406  lpbl  18538  met2ndci  18557  prdsxmslem2  18564  metustexhalfOLD  18598  metustexhalf  18599  metutopOLD  18617  psmetutop  18618  tgioo  18832  metdstri  18886  metdseq0  18889  xlebnum  18995  clsocv  19209  metelcls  19262  cmetss  19272  relcmpcmet  19274  cmpcmet  19275  minveclem4a  19336  uniioovol  19476  uniioombllem3  19482  limcres  19778  dvbss  19793  perfdvf  19795  dvreslem  19801  dvres2lem  19802  dvcnp2  19811  dvaddbr  19829  dvmulbr  19830  dvcmulf  19836  dvcj  19841  dvnfre  19843  dvmptres2  19853  dvmptcmul  19855  dvmptntr  19862  dvlip2  19884  dvcnvrelem2  19907  ftc1cn  19932  taylfvallem1  20278  taylply2  20289  taylply  20290  dvtaylp  20291  dvntaylp  20292  dvntaylp0  20293  taylthlem1  20294  taylthlem2  20295  ulmdvlem3  20323  pserulm  20343  shsub2  22832  spanssoc  22856  shub2  22890  ococin  22915  ssjo  22954  chub2  23015  spanpr  23087  elnlfn  23436  mdslj1i  23827  mdslmd3i  23840  mdexchi  23843  chirredlem1  23898  atcvat3i  23904  mdsymlem1  23911  mdsymlem5  23915  imadifxp  24043  sitgclg  24661  cvmscld  24965  cvmliftmolem1  24973  cvmlift2lem9  25003  cvmlift2lem11  25005  cvmlift3lem6  25016  prodss  25278  nodense  25649  ftc1cnnc  26292  opnregcld  26346  ivthALT  26351  neibastop2  26403  fnemeet1  26408  fnejoin1  26410  sstotbnd  26497  ssbnd  26510  heibor1lem  26531  heiborlem3  26535  heibor  26543  ismrcd1  26765  ismrcd2  26766  coeq0i  26824  lsslindf  27290  hbtlem6  27323  rgspnval  27363  lsmsat  29879  lssats  29883  lcvexchlem3  29907  lsatcvat3  29923  lkrscss  29969  lkrpssN  30034  pmod1i  30718  pclbtwnN  30767  pclunN  30768  pclss2polN  30791  pcl0N  30792  sspmaplubN  30795  paddunN  30797  pnonsingN  30803  pclfinclN  30820  osumcllem4N  30829  dia2dimlem13  31947  dvhopellsm  31988  dvadiaN  31999  dicelval1stN  32059  dicelval2nd  32060  dihssxp  32123  dihvalrel  32150  dochsscl  32239  dihoml4  32248  dochnoncon  32262  dvh3dim3N  32320  lcfrlem2  32414  lcfrlem5  32417  lcfr  32456  lcdlsp  32492  mapdsn  32512  mapdlsm  32535  mapdpglem1  32543  mapdindp0  32590  hlhilocv  32831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator