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

Theorem sseqtrd 3453
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 3445 . 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 1399    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  sseqtr4d  3454  uniintsn  4237  oeeui  7169  nnaword2  7197  oaabs2  7212  erssxp  7252  fipwuni  7801  ordtypelem7  7864  cantnflem3  8023  cantnflem3OLD  8045  cdainf  8485  ficardun2  8496  ackbij1lem12  8524  ackbij1b  8532  fin1a2lem13  8705  winafp  8986  ioodisj  11571  reltrclfv  12855  prodss  13756  vdwlem11  14511  mrcssv  15021  mrcsscl  15027  mrcuni  15028  mressmrcd  15034  mreexexlem2d  15052  mreexexlem3d  15053  mreexfidimd  15057  subcss2  15249  resssetc  15488  funcsetcres2  15489  estrres  15525  poslubdg  15896  ipodrsfi  15910  acsmap2d  15926  mrelatlub  15933  mreclatBAD  15934  subsubm  16105  subsubg  16341  oppglsm  16779  subglsm  16808  lsmdisj  16816  gsumval3OLD  17025  gsumval3  17028  dprdres  17188  dprdss  17189  dprd2da  17204  dmdprdsplit2lem  17207  ablfac1b  17234  pgpfac1lem3  17241  issubdrg  17567  subsubrg  17568  islssd  17695  lspun  17746  lspssp  17747  lsslsp  17774  lsmssspx  17847  lspabs2  17879  lspabs3  17880  lspsolvlem  17901  lbsextlem3  17919  mplbas2  18247  mplbas2OLD  18248  gsumply1subr  18388  qsssubdrg  18590  obselocv  18850  lsslindf  18950  tgcl  19556  basgen  19575  tgfiss  19578  bastop1  19580  bastop2  19581  clsss2  19659  elcls3  19670  topssnei  19711  neiptopnei  19719  neitr  19767  restcls  19768  restlp  19770  ordtrest2  19791  iscncl  19856  cncls2  19860  cncls  19861  cnntr  19862  lmcls  19889  tgcmp  19987  cmpcld  19988  uncmp  19989  hauscmplem  19992  cmpfi  19994  clscon  20016  2ndcsb  20035  2ndcctbss  20041  2ndcomap  20044  nllyrest  20072  1stckgenlem  20139  kgencn2  20143  kgen2cn  20145  ptbasfi  20167  txcld  20189  txcls  20190  txbasval  20192  neitx  20193  ptcld  20199  ptclsg  20201  txnlly  20223  hausdiag  20231  txkgen  20238  xkopt  20241  xkopjcn  20242  xkococnlem  20245  cnmpt1res  20262  cnmpt2res  20263  imasnopn  20276  imasncld  20277  imasncls  20278  qtopcld  20299  qtoprest  20303  qtopcmap  20305  kqcldsat  20319  kqreglem2  20328  kqnrmlem2  20330  hmeontr  20355  neifil  20466  fgtr  20476  trnei  20478  uffixfr  20509  uffix2  20510  uffixsn  20511  elflim  20557  flimclslem  20570  fclsopn  20600  fclscmpi  20615  fclscmp  20616  alexsubALTlem3  20634  alexsubALT  20636  ptcmplem3  20639  subgntr  20690  opnsubg  20691  clssubg  20692  clsnsg  20693  cldsubg  20694  tgpconcompeqg  20695  snclseqg  20699  tsmsgsum  20722  tsmsid  20723  tsmsgsumOLD  20725  tsmsidOLD  20726  tgptsmscld  20738  ustssco  20802  utop2nei  20838  utop3cls  20839  utopreg  20840  cnextucn  20891  ressprdsds  20959  lpbl  21091  met2ndci  21110  prdsxmslem2  21117  metustexhalfOLD  21151  metustexhalf  21152  metutopOLD  21170  psmetutop  21171  tgioo  21386  metdstri  21440  metdseq0  21443  xlebnum  21550  clsocv  21775  metelcls  21828  cmetss  21838  relcmpcmet  21840  cmpcmet  21841  minveclem4a  21930  uniioovol  22073  uniioombllem3  22079  limcres  22375  dvbss  22390  perfdvf  22392  dvreslem  22398  dvres2lem  22399  dvcnp2  22408  dvaddbr  22426  dvmulbr  22427  dvcmulf  22433  dvcj  22438  dvnfre  22440  dvmptres2  22450  dvmptcmul  22452  dvmptntr  22459  dvlip2  22481  dvcnvrelem2  22504  ftc1cn  22529  taylfvallem1  22837  taylply2  22848  taylply  22849  dvtaylp  22850  dvntaylp  22851  dvntaylp0  22852  taylthlem1  22853  taylthlem2  22854  ulmdvlem3  22882  pserulm  22902  shsub2  26360  spanssoc  26384  shub2  26418  ococin  26443  ssjo  26482  chub2  26543  spanpr  26615  elnlfn  26963  mdslj1i  27354  mdslmd3i  27367  mdexchi  27370  chirredlem1  27425  atcvat3i  27431  mdsymlem1  27438  mdsymlem5  27442  rntrclfvOAI  27478  imadifxp  27591  qtophaus  27993  locfinreflem  27997  fsumcvg4  28086  esum2d  28241  omsmon  28425  omssubadd  28427  carsggect  28445  carsgclctun  28448  sitgclg  28467  eulerpartlemgf  28501  cvmscld  28907  cvmliftmolem1  28915  cvmlift2lem9  28945  cvmlift2lem11  28947  cvmlift3lem6  28958  nodense  29614  ftc1cnnc  30255  opnregcld  30314  ivthALT  30319  neibastop2  30345  fnemeet1  30350  fnejoin1  30352  sstotbnd  30437  ssbnd  30450  heibor1lem  30471  heiborlem3  30475  heibor  30483  ismrcd1  30796  ismrcd2  30797  coeq0i  30851  hbtlem6  31246  rgspnval  31285  iocinico  31347  iccdifprioo  31722  cncfuni  31855  cncfiooicclem1  31862  dvresntr  31879  dvmptresicc  31882  itgsubsticclem  31940  fourierdlem42  32097  fourierdlem48  32103  fourierdlem49  32104  fourierdlem50  32105  subsubmgm  32803  lsmsat  35146  lssats  35150  lcvexchlem3  35174  lsatcvat3  35190  lkrscss  35236  lkrpssN  35301  pmod1i  35985  pclbtwnN  36034  pclunN  36035  pclss2polN  36058  pcl0N  36059  sspmaplubN  36062  paddunN  36064  pnonsingN  36070  pclfinclN  36087  osumcllem4N  36096  dia2dimlem13  37216  dvhopellsm  37257  dvadiaN  37268  dicelval1stN  37328  dicelval2nd  37329  dihssxp  37392  dihvalrel  37419  dochsscl  37508  dihoml4  37517  dochnoncon  37531  dvh3dim3N  37589  lcfrlem2  37683  lcfrlem5  37686  lcfr  37725  lcdlsp  37761  mapdsn  37781  mapdlsm  37804  mapdpglem1  37812  mapdindp0  37859  hlhilocv  38100
  Copyright terms: Public domain W3C validator