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

Theorem sseqtrd 3499
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 3491 . 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 1370    C_ wss 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449
This theorem is referenced by:  sseqtr4d  3500  uniintsn  4272  oeeui  7150  nnaword2  7178  oaabs2  7193  erssxp  7233  fipwuni  7786  ordtypelem7  7848  cantnflem3  8009  cantnflem3OLD  8031  cdainf  8471  ficardun2  8482  ackbij1lem12  8510  ackbij1b  8518  fin1a2lem13  8691  winafp  8974  ioodisj  11531  vdwlem11  14169  mrcssv  14670  mrcsscl  14676  mrcuni  14677  mressmrcd  14683  mreexexlem2d  14701  mreexexlem3d  14702  mreexfidimd  14706  subcss2  14871  resssetc  15078  funcsetcres2  15079  poslubdg  15437  ipodrsfi  15451  acsmap2d  15467  mrelatlub  15474  mreclatBAD  15475  subsubm  15603  subsubg  15822  oppglsm  16261  subglsm  16290  lsmdisj  16298  gsumval3OLD  16502  gsumval3  16505  dprdres  16646  dprdss  16647  dprd2da  16662  dmdprdsplit2lem  16665  ablfac1b  16692  pgpfac1lem3  16699  issubdrg  17012  subsubrg  17013  islssd  17139  lspun  17190  lspssp  17191  lsslsp  17218  lsmssspx  17291  lspabs2  17323  lspabs3  17324  lspsolvlem  17345  lbsextlem3  17363  mplbas2  17674  mplbas2OLD  17675  gsumply1subr  17811  qsssubdrg  17996  obselocv  18277  lsslindf  18383  tgcl  18705  basgen  18724  tgfiss  18727  bastop1  18729  bastop2  18730  clsss2  18807  elcls3  18818  topssnei  18859  neiptopnei  18867  neitr  18915  restcls  18916  restlp  18918  ordtrest2  18939  iscncl  19004  cncls2  19008  cncls  19009  cnntr  19010  lmcls  19037  tgcmp  19135  cmpcld  19136  uncmp  19137  hauscmplem  19140  cmpfi  19142  clscon  19165  2ndcsb  19184  2ndcctbss  19190  2ndcomap  19193  nllyrest  19221  1stckgenlem  19257  kgencn2  19261  kgen2cn  19263  ptbasfi  19285  txcld  19307  txcls  19308  txbasval  19310  neitx  19311  ptcld  19317  ptclsg  19319  txnlly  19341  hausdiag  19349  txkgen  19356  xkopt  19359  xkopjcn  19360  xkococnlem  19363  cnmpt1res  19380  cnmpt2res  19381  imasnopn  19394  imasncld  19395  imasncls  19396  qtopcld  19417  qtoprest  19421  qtopcmap  19423  kqcldsat  19437  kqreglem2  19446  kqnrmlem2  19448  hmeontr  19473  neifil  19584  fgtr  19594  trnei  19596  uffixfr  19627  uffix2  19628  uffixsn  19629  elflim  19675  flimclslem  19688  fclsopn  19718  fclscmpi  19733  fclscmp  19734  alexsubALTlem3  19752  alexsubALT  19754  ptcmplem3  19757  subgntr  19808  opnsubg  19809  clssubg  19810  clsnsg  19811  cldsubg  19812  tgpconcompeqg  19813  snclseqg  19817  tsmsgsum  19840  tsmsid  19841  tsmsgsumOLD  19843  tsmsidOLD  19844  tgptsmscld  19856  ustssco  19920  utop2nei  19956  utop3cls  19957  utopreg  19958  cnextucn  20009  ressprdsds  20077  lpbl  20209  met2ndci  20228  prdsxmslem2  20235  metustexhalfOLD  20269  metustexhalf  20270  metutopOLD  20288  psmetutop  20289  tgioo  20504  metdstri  20558  metdseq0  20561  xlebnum  20668  clsocv  20893  metelcls  20946  cmetss  20956  relcmpcmet  20958  cmpcmet  20959  minveclem4a  21048  uniioovol  21191  uniioombllem3  21197  limcres  21493  dvbss  21508  perfdvf  21510  dvreslem  21516  dvres2lem  21517  dvcnp2  21526  dvaddbr  21544  dvmulbr  21545  dvcmulf  21551  dvcj  21556  dvnfre  21558  dvmptres2  21568  dvmptcmul  21570  dvmptntr  21577  dvlip2  21599  dvcnvrelem2  21622  ftc1cn  21647  taylfvallem1  21954  taylply2  21965  taylply  21966  dvtaylp  21967  dvntaylp  21968  dvntaylp0  21969  taylthlem1  21970  taylthlem2  21971  ulmdvlem3  21999  pserulm  22019  shsub2  24879  spanssoc  24903  shub2  24937  ococin  24962  ssjo  25001  chub2  25062  spanpr  25134  elnlfn  25483  mdslj1i  25874  mdslmd3i  25887  mdexchi  25890  chirredlem1  25945  atcvat3i  25951  mdsymlem1  25958  mdsymlem5  25962  imadifxp  26089  fsumcvg4  26524  omsfval  26852  omsmon  26854  sitgclg  26871  eulerpartlemgf  26905  cvmscld  27305  cvmliftmolem1  27313  cvmlift2lem9  27343  cvmlift2lem11  27345  cvmlift3lem6  27356  prodss  27603  nodense  27973  ftc1cnnc  28613  opnregcld  28672  ivthALT  28677  neibastop2  28729  fnemeet1  28734  fnejoin1  28736  sstotbnd  28821  ssbnd  28834  heibor1lem  28855  heiborlem3  28859  heibor  28867  ismrcd1  29181  ismrcd2  29182  coeq0i  29238  hbtlem6  29632  rgspnval  29672  iocinico  29734  lsmsat  32976  lssats  32980  lcvexchlem3  33004  lsatcvat3  33020  lkrscss  33066  lkrpssN  33131  pmod1i  33815  pclbtwnN  33864  pclunN  33865  pclss2polN  33888  pcl0N  33889  sspmaplubN  33892  paddunN  33894  pnonsingN  33900  pclfinclN  33917  osumcllem4N  33926  dia2dimlem13  35044  dvhopellsm  35085  dvadiaN  35096  dicelval1stN  35156  dicelval2nd  35157  dihssxp  35220  dihvalrel  35247  dochsscl  35336  dihoml4  35345  dochnoncon  35359  dvh3dim3N  35417  lcfrlem2  35511  lcfrlem5  35514  lcfr  35553  lcdlsp  35589  mapdsn  35609  mapdlsm  35632  mapdpglem1  35640  mapdindp0  35687  hlhilocv  35928
  Copyright terms: Public domain W3C validator