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

Theorem sseqtrd 3540
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 3532 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sseqtr4d  3541  uniintsn  4319  oeeui  7251  nnaword2  7279  oaabs2  7294  erssxp  7334  fipwuni  7886  ordtypelem7  7949  cantnflem3  8110  cantnflem3OLD  8132  cdainf  8572  ficardun2  8583  ackbij1lem12  8611  ackbij1b  8619  fin1a2lem13  8792  winafp  9075  ioodisj  11650  vdwlem11  14368  mrcssv  14869  mrcsscl  14875  mrcuni  14876  mressmrcd  14882  mreexexlem2d  14900  mreexexlem3d  14901  mreexfidimd  14905  subcss2  15070  resssetc  15277  funcsetcres2  15278  poslubdg  15636  ipodrsfi  15650  acsmap2d  15666  mrelatlub  15673  mreclatBAD  15674  subsubm  15807  subsubg  16029  oppglsm  16468  subglsm  16497  lsmdisj  16505  gsumval3OLD  16711  gsumval3  16714  dprdres  16877  dprdss  16878  dprd2da  16893  dmdprdsplit2lem  16896  ablfac1b  16923  pgpfac1lem3  16930  issubdrg  17254  subsubrg  17255  islssd  17382  lspun  17433  lspssp  17434  lsslsp  17461  lsmssspx  17534  lspabs2  17566  lspabs3  17567  lspsolvlem  17588  lbsextlem3  17606  mplbas2  17933  mplbas2OLD  17934  gsumply1subr  18074  qsssubdrg  18273  obselocv  18554  lsslindf  18660  tgcl  19265  basgen  19284  tgfiss  19287  bastop1  19289  bastop2  19290  clsss2  19367  elcls3  19378  topssnei  19419  neiptopnei  19427  neitr  19475  restcls  19476  restlp  19478  ordtrest2  19499  iscncl  19564  cncls2  19568  cncls  19569  cnntr  19570  lmcls  19597  tgcmp  19695  cmpcld  19696  uncmp  19697  hauscmplem  19700  cmpfi  19702  clscon  19725  2ndcsb  19744  2ndcctbss  19750  2ndcomap  19753  nllyrest  19781  1stckgenlem  19817  kgencn2  19821  kgen2cn  19823  ptbasfi  19845  txcld  19867  txcls  19868  txbasval  19870  neitx  19871  ptcld  19877  ptclsg  19879  txnlly  19901  hausdiag  19909  txkgen  19916  xkopt  19919  xkopjcn  19920  xkococnlem  19923  cnmpt1res  19940  cnmpt2res  19941  imasnopn  19954  imasncld  19955  imasncls  19956  qtopcld  19977  qtoprest  19981  qtopcmap  19983  kqcldsat  19997  kqreglem2  20006  kqnrmlem2  20008  hmeontr  20033  neifil  20144  fgtr  20154  trnei  20156  uffixfr  20187  uffix2  20188  uffixsn  20189  elflim  20235  flimclslem  20248  fclsopn  20278  fclscmpi  20293  fclscmp  20294  alexsubALTlem3  20312  alexsubALT  20314  ptcmplem3  20317  subgntr  20368  opnsubg  20369  clssubg  20370  clsnsg  20371  cldsubg  20372  tgpconcompeqg  20373  snclseqg  20377  tsmsgsum  20400  tsmsid  20401  tsmsgsumOLD  20403  tsmsidOLD  20404  tgptsmscld  20416  ustssco  20480  utop2nei  20516  utop3cls  20517  utopreg  20518  cnextucn  20569  ressprdsds  20637  lpbl  20769  met2ndci  20788  prdsxmslem2  20795  metustexhalfOLD  20829  metustexhalf  20830  metutopOLD  20848  psmetutop  20849  tgioo  21064  metdstri  21118  metdseq0  21121  xlebnum  21228  clsocv  21453  metelcls  21506  cmetss  21516  relcmpcmet  21518  cmpcmet  21519  minveclem4a  21608  uniioovol  21751  uniioombllem3  21757  limcres  22053  dvbss  22068  perfdvf  22070  dvreslem  22076  dvres2lem  22077  dvcnp2  22086  dvaddbr  22104  dvmulbr  22105  dvcmulf  22111  dvcj  22116  dvnfre  22118  dvmptres2  22128  dvmptcmul  22130  dvmptntr  22137  dvlip2  22159  dvcnvrelem2  22182  ftc1cn  22207  taylfvallem1  22514  taylply2  22525  taylply  22526  dvtaylp  22527  dvntaylp  22528  dvntaylp0  22529  taylthlem1  22530  taylthlem2  22531  ulmdvlem3  22559  pserulm  22579  shsub2  25947  spanssoc  25971  shub2  26005  ococin  26030  ssjo  26069  chub2  26130  spanpr  26202  elnlfn  26551  mdslj1i  26942  mdslmd3i  26955  mdexchi  26958  chirredlem1  27013  atcvat3i  27019  mdsymlem1  27026  mdsymlem5  27030  imadifxp  27159  fsumcvg4  27596  qtophaus  27665  omsfval  27933  omsmon  27935  sitgclg  27952  eulerpartlemgf  27986  cvmscld  28386  cvmliftmolem1  28394  cvmlift2lem9  28424  cvmlift2lem11  28426  cvmlift3lem6  28437  prodss  28684  nodense  29054  ftc1cnnc  29694  opnregcld  29753  ivthALT  29758  neibastop2  29810  fnemeet1  29815  fnejoin1  29817  sstotbnd  29902  ssbnd  29915  heibor1lem  29936  heiborlem3  29940  heibor  29948  ismrcd1  30262  ismrcd2  30263  coeq0i  30318  hbtlem6  30710  rgspnval  30750  iocinico  30812  iccdifprioo  31148  cncfuni  31253  cncfiooicclem1  31260  dvsinax  31269  dvresntr  31274  dvmptresicc  31277  dvbdfbdioolem1  31286  itgcoscmulx  31315  itgsubsticclem  31321  fourierdlem42  31477  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem70  31505  fourierdlem71  31506  fourierdlem74  31509  fourierdlem103  31538  fourierdlem104  31539  fourierdlem113  31548  fouriercn  31561  lsmsat  33823  lssats  33827  lcvexchlem3  33851  lsatcvat3  33867  lkrscss  33913  lkrpssN  33978  pmod1i  34662  pclbtwnN  34711  pclunN  34712  pclss2polN  34735  pcl0N  34736  sspmaplubN  34739  paddunN  34741  pnonsingN  34747  pclfinclN  34764  osumcllem4N  34773  dia2dimlem13  35891  dvhopellsm  35932  dvadiaN  35943  dicelval1stN  36003  dicelval2nd  36004  dihssxp  36067  dihvalrel  36094  dochsscl  36183  dihoml4  36192  dochnoncon  36206  dvh3dim3N  36264  lcfrlem2  36358  lcfrlem5  36361  lcfr  36400  lcdlsp  36436  mapdsn  36456  mapdlsm  36479  mapdpglem1  36487  mapdindp0  36534  hlhilocv  36775
  Copyright terms: Public domain W3C validator