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

Theorem sseqtrd 3376
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 3368 . 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 1652    C_ wss 3312
This theorem is referenced by:  sseqtr4d  3377  uniintsn  4079  oeeui  6837  nnaword2  6865  oaabs2  6880  erssxp  6920  fipwuni  7423  ordtypelem7  7485  cantnflem3  7639  cdainf  8064  ficardun2  8075  ackbij1lem12  8103  ackbij1b  8111  fin1a2lem13  8284  winafp  8564  ioodisj  11018  vdwlem11  13351  mrcssv  13831  mrcsscl  13837  mrcuni  13838  mressmrcd  13844  mreexexlem2d  13862  mreexexlem3d  13863  mreexfidimd  13867  subcss2  14032  resssetc  14239  funcsetcres2  14240  poslubdg  14567  ipodrsfi  14581  acsmap2d  14597  mrelatlub  14604  mreclat  14605  subsubm  14749  subsubg  14955  oppglsm  15268  subglsm  15297  lsmdisj  15305  gsumval3  15506  dprdres  15578  dprdss  15579  dprd2da  15592  dmdprdsplit2lem  15595  ablfac1b  15620  pgpfac1lem3  15627  issubdrg  15885  subsubrg  15886  islssd  16004  lspun  16055  lspssp  16056  lsslsp  16083  lsmssspx  16152  lspabs2  16184  lspabs3  16185  lspsolvlem  16206  lbsextlem3  16224  mplbas2  16523  qsssubdrg  16750  obselocv  16947  tgcl  17026  basgen  17045  tgfiss  17048  bastop1  17050  bastop2  17051  clsss2  17128  elcls3  17139  topssnei  17180  neiptopnei  17188  neitr  17236  restcls  17237  restlp  17239  ordtrest2  17260  iscncl  17325  cncls2  17329  cncls  17330  cnntr  17331  lmcls  17358  tgcmp  17456  cmpcld  17457  uncmp  17458  hauscmplem  17461  cmpfi  17463  clscon  17485  2ndcsb  17504  2ndcctbss  17510  2ndcomap  17513  nllyrest  17541  1stckgenlem  17577  kgencn2  17581  kgen2cn  17583  ptbasfi  17605  txcld  17627  txcls  17628  txbasval  17630  neitx  17631  ptcld  17637  ptclsg  17639  txnlly  17661  hausdiag  17669  txkgen  17676  xkopt  17679  xkopjcn  17680  xkococnlem  17683  cnmpt1res  17700  cnmpt2res  17701  imasnopn  17714  imasncld  17715  imasncls  17716  qtopcld  17737  qtoprest  17741  qtopcmap  17743  kqcldsat  17757  kqreglem2  17766  kqnrmlem2  17768  hmeontr  17793  neifil  17904  fgtr  17914  trnei  17916  uffixfr  17947  uffix2  17948  uffixsn  17949  elflim  17995  flimclslem  18008  fclsopn  18038  fclscmpi  18053  fclscmp  18054  alexsubALTlem3  18072  alexsubALT  18074  ptcmplem3  18077  subgntr  18128  opnsubg  18129  clssubg  18130  clsnsg  18131  cldsubg  18132  tgpconcompeqg  18133  snclseqg  18137  tsmsgsum  18160  tsmsid  18161  tgptsmscld  18172  ustssco  18236  utop2nei  18272  utop3cls  18273  utopreg  18274  cnextucn  18325  ressprdsds  18393  lpbl  18525  met2ndci  18544  prdsxmslem2  18551  metustexhalfOLD  18585  metustexhalf  18586  metutopOLD  18604  psmetutop  18605  tgioo  18819  metdstri  18873  metdseq0  18876  xlebnum  18982  clsocv  19196  metelcls  19249  cmetss  19259  relcmpcmet  19261  cmpcmet  19262  minveclem4a  19323  uniioovol  19463  uniioombllem3  19469  limcres  19765  dvbss  19780  perfdvf  19782  dvreslem  19788  dvres2lem  19789  dvcnp2  19798  dvaddbr  19816  dvmulbr  19817  dvcmulf  19823  dvcj  19828  dvnfre  19830  dvmptres2  19840  dvmptcmul  19842  dvmptntr  19849  dvlip2  19871  dvcnvrelem2  19894  ftc1cn  19919  taylfvallem1  20265  taylply2  20276  taylply  20277  dvtaylp  20278  dvntaylp  20279  dvntaylp0  20280  taylthlem1  20281  taylthlem2  20282  ulmdvlem3  20310  pserulm  20330  shsub2  22819  spanssoc  22843  shub2  22877  ococin  22902  ssjo  22941  chub2  23002  spanpr  23074  elnlfn  23423  mdslj1i  23814  mdslmd3i  23827  mdexchi  23830  chirredlem1  23885  atcvat3i  23891  mdsymlem1  23898  mdsymlem5  23902  imadifxp  24030  sitgclg  24648  cvmscld  24952  cvmliftmolem1  24960  cvmlift2lem9  24990  cvmlift2lem11  24992  cvmlift3lem6  25003  prodss  25265  nodense  25636  ftc1cnnc  26269  opnregcld  26324  ivthALT  26329  neibastop2  26381  fnemeet1  26386  fnejoin1  26388  sstotbnd  26475  ssbnd  26488  heibor1lem  26509  heiborlem3  26513  heibor  26521  ismrcd1  26743  ismrcd2  26744  coeq0i  26802  lsslindf  27268  hbtlem6  27301  rgspnval  27341  lsmsat  29743  lssats  29747  lcvexchlem3  29771  lsatcvat3  29787  lkrscss  29833  lkrpssN  29898  pmod1i  30582  pclbtwnN  30631  pclunN  30632  pclss2polN  30655  pcl0N  30656  sspmaplubN  30659  paddunN  30661  pnonsingN  30667  pclfinclN  30684  osumcllem4N  30693  dia2dimlem13  31811  dvhopellsm  31852  dvadiaN  31863  dicelval1stN  31923  dicelval2nd  31924  dihssxp  31987  dihvalrel  32014  dochsscl  32103  dihoml4  32112  dochnoncon  32126  dvh3dim3N  32184  lcfrlem2  32278  lcfrlem5  32281  lcfr  32320  lcdlsp  32356  mapdsn  32376  mapdlsm  32399  mapdpglem1  32407  mapdindp0  32454  hlhilocv  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator