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

Theorem sseqtrd 3387
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 3379 . 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 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sseqtr4d  3388  uniintsn  4160  oeeui  7033  nnaword2  7061  oaabs2  7076  erssxp  7116  fipwuni  7668  ordtypelem7  7730  cantnflem3  7891  cantnflem3OLD  7913  cdainf  8353  ficardun2  8364  ackbij1lem12  8392  ackbij1b  8400  fin1a2lem13  8573  winafp  8856  ioodisj  11407  vdwlem11  14044  mrcssv  14544  mrcsscl  14550  mrcuni  14551  mressmrcd  14557  mreexexlem2d  14575  mreexexlem3d  14576  mreexfidimd  14580  subcss2  14745  resssetc  14952  funcsetcres2  14953  poslubdg  15311  ipodrsfi  15325  acsmap2d  15341  mrelatlub  15348  mreclatBAD  15349  subsubm  15476  subsubg  15695  oppglsm  16132  subglsm  16161  lsmdisj  16169  gsumval3OLD  16373  gsumval3  16376  dprdres  16515  dprdss  16516  dprd2da  16531  dmdprdsplit2lem  16534  ablfac1b  16561  pgpfac1lem3  16568  issubdrg  16870  subsubrg  16871  islssd  16997  lspun  17048  lspssp  17049  lsslsp  17076  lsmssspx  17149  lspabs2  17181  lspabs3  17182  lspsolvlem  17203  lbsextlem3  17221  mplbas2  17531  mplbas2OLD  17532  gsumply1subr  17668  qsssubdrg  17852  obselocv  18133  lsslindf  18239  tgcl  18554  basgen  18573  tgfiss  18576  bastop1  18578  bastop2  18579  clsss2  18656  elcls3  18667  topssnei  18708  neiptopnei  18716  neitr  18764  restcls  18765  restlp  18767  ordtrest2  18788  iscncl  18853  cncls2  18857  cncls  18858  cnntr  18859  lmcls  18886  tgcmp  18984  cmpcld  18985  uncmp  18986  hauscmplem  18989  cmpfi  18991  clscon  19014  2ndcsb  19033  2ndcctbss  19039  2ndcomap  19042  nllyrest  19070  1stckgenlem  19106  kgencn2  19110  kgen2cn  19112  ptbasfi  19134  txcld  19156  txcls  19157  txbasval  19159  neitx  19160  ptcld  19166  ptclsg  19168  txnlly  19190  hausdiag  19198  txkgen  19205  xkopt  19208  xkopjcn  19209  xkococnlem  19212  cnmpt1res  19229  cnmpt2res  19230  imasnopn  19243  imasncld  19244  imasncls  19245  qtopcld  19266  qtoprest  19270  qtopcmap  19272  kqcldsat  19286  kqreglem2  19295  kqnrmlem2  19297  hmeontr  19322  neifil  19433  fgtr  19443  trnei  19445  uffixfr  19476  uffix2  19477  uffixsn  19478  elflim  19524  flimclslem  19537  fclsopn  19567  fclscmpi  19582  fclscmp  19583  alexsubALTlem3  19601  alexsubALT  19603  ptcmplem3  19606  subgntr  19657  opnsubg  19658  clssubg  19659  clsnsg  19660  cldsubg  19661  tgpconcompeqg  19662  snclseqg  19666  tsmsgsum  19689  tsmsid  19690  tsmsgsumOLD  19692  tsmsidOLD  19693  tgptsmscld  19705  ustssco  19769  utop2nei  19805  utop3cls  19806  utopreg  19807  cnextucn  19858  ressprdsds  19926  lpbl  20058  met2ndci  20077  prdsxmslem2  20084  metustexhalfOLD  20118  metustexhalf  20119  metutopOLD  20137  psmetutop  20138  tgioo  20353  metdstri  20407  metdseq0  20410  xlebnum  20517  clsocv  20742  metelcls  20795  cmetss  20805  relcmpcmet  20807  cmpcmet  20808  minveclem4a  20897  uniioovol  21039  uniioombllem3  21045  limcres  21341  dvbss  21356  perfdvf  21358  dvreslem  21364  dvres2lem  21365  dvcnp2  21374  dvaddbr  21392  dvmulbr  21393  dvcmulf  21399  dvcj  21404  dvnfre  21406  dvmptres2  21416  dvmptcmul  21418  dvmptntr  21425  dvlip2  21447  dvcnvrelem2  21470  ftc1cn  21495  taylfvallem1  21802  taylply2  21813  taylply  21814  dvtaylp  21815  dvntaylp  21816  dvntaylp0  21817  taylthlem1  21818  taylthlem2  21819  ulmdvlem3  21847  pserulm  21867  shsub2  24696  spanssoc  24720  shub2  24754  ococin  24779  ssjo  24818  chub2  24879  spanpr  24951  elnlfn  25300  mdslj1i  25691  mdslmd3i  25704  mdexchi  25707  chirredlem1  25762  atcvat3i  25768  mdsymlem1  25775  mdsymlem5  25779  imadifxp  25907  fsumcvg4  26349  omsfval  26678  omsmon  26680  sitgclg  26697  eulerpartlemgf  26731  cvmscld  27131  cvmliftmolem1  27139  cvmlift2lem9  27169  cvmlift2lem11  27171  cvmlift3lem6  27182  prodss  27429  nodense  27799  ftc1cnnc  28437  opnregcld  28496  ivthALT  28501  neibastop2  28553  fnemeet1  28558  fnejoin1  28560  sstotbnd  28645  ssbnd  28658  heibor1lem  28679  heiborlem3  28683  heibor  28691  ismrcd1  29005  ismrcd2  29006  coeq0i  29062  hbtlem6  29456  rgspnval  29496  iocinico  29558  lsmsat  32546  lssats  32550  lcvexchlem3  32574  lsatcvat3  32590  lkrscss  32636  lkrpssN  32701  pmod1i  33385  pclbtwnN  33434  pclunN  33435  pclss2polN  33458  pcl0N  33459  sspmaplubN  33462  paddunN  33464  pnonsingN  33470  pclfinclN  33487  osumcllem4N  33496  dia2dimlem13  34614  dvhopellsm  34655  dvadiaN  34666  dicelval1stN  34726  dicelval2nd  34727  dihssxp  34790  dihvalrel  34817  dochsscl  34906  dihoml4  34915  dochnoncon  34929  dvh3dim3N  34987  lcfrlem2  35081  lcfrlem5  35084  lcfr  35123  lcdlsp  35159  mapdsn  35179  mapdlsm  35202  mapdpglem1  35210  mapdindp0  35257  hlhilocv  35498
  Copyright terms: Public domain W3C validator