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

Theorem sseqtri 3210
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
Hypotheses
Ref Expression
sseqtr.1  |-  A  C_  B
sseqtr.2  |-  B  =  C
Assertion
Ref Expression
sseqtri  |-  A  C_  C

Proof of Theorem sseqtri
StepHypRef Expression
1 sseqtr.1 . 2  |-  A  C_  B
2 sseqtr.2 . . 3  |-  B  =  C
32sseq2i 3203 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 199 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3152
This theorem is referenced by:  sseqtr4i  3211  eqimssi  3232  abssi  3248  ssun2  3339  difex2  4525  unixpss  4799  0ima  5031  fvssunirn  5551  oelim2  6593  omopthlem2  6654  sbthlem7  6977  unifpw  7158  fiuni  7181  rankuni  7535  rankc2  7543  rankxpu  7548  rankxplim  7549  infxpenlem  7641  cf0  7877  fin23lem17  7964  fin23lem31  7969  smobeth  8208  nqerf  8554  dmrecnq  8592  ackbijnn  12286  divalglem2  12594  divalglem5  12596  bitsfzolem  12625  0bits  12630  bezoutlem2  12718  bezoutlem3  12719  odzcllem  12857  odzdvds  12860  unbenlem  12955  4sqlem13  13004  4sqlem14  13005  4sqlem17  13008  4sqlem18  13009  vdwlem8  13035  vdwnnlem3  13044  ramcl2lem  13056  ramtcl  13057  ramtub  13059  strle1  13239  prdsval  13355  xpsc0  13462  xpsc1  13463  wunfunc  13773  wunnat  13830  psssdm2  14324  tsrss  14332  gicer  14740  odlem2  14854  gexlem2  14893  torsubg  15146  gsumzaddlem  15203  dprd2da  15277  zlpirlem2  16442  zlpirlem3  16443  pjfval  16606  pjpm  16608  eltg4i  16698  ntrss2  16794  isopn3  16803  mretopd  16829  leordtval2  16942  ptbasfi  17276  hmphtop  17469  hmpher  17475  tngtopn  18166  tgioo  18302  xrtgioo  18312  iccpnfcnv  18442  ovolicc2lem4  18879  nulmbl2  18894  iundisj  18905  dyadmax  18953  i1f1  19045  dvfval  19247  dvcnp2  19269  lhop1lem  19360  lhop2  19362  elqaalem1  19699  elqaalem3  19701  taylthlem2  19753  pserulm  19798  psercn2  19799  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  pserdv  19805  pserdv2  19806  abelth  19817  dvlog  19998  efopnlem2  20004  logtayl  20007  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  dvatan  20231  atancn  20232  rlimcnp  20260  rlimcnp2  20261  wilthlem2  20307  wilthlem3  20308  ftalem4  20313  ftalem5  20314  dchrisum0lem2a  20666  choc1  21906  chub2i  22049  span0  22121  spanuni  22123  sshhococi  22125  chsup0  22127  spansnpji  22157  mayetes3i  22309  nlelshi  22640  pjimai  22756  pj3i  22788  shatomistici  22941  hatomistici  22942  atcvat4i  22977  ballotlemfmpn  23053  xrge0mulgnn0  23313  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  xrge0adddir  23332  fsumrp0cl  23334  mptctf  23348  iundisjfi  23363  iundisjf  23365  lmlimxrge0  23372  rge0scvg  23373  lmdvg  23376  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumpcvgval  23446  esumcvg  23454  coinfliprv  23683  kur14lem6  23742  nocvxminlem  24344  nocvxmin  24345  nobndlem1  24346  nobndlem2  24347  axlowdimlem6  24575  onint1  24888  oninhaus  24889  reldded  25741  relrded  25742  reldcat  25762  relrcat  25763  filnetlem3  26329  filnetlem4  26330  heiborlem3  26537  isdrngo2  26589  elrfi  26769  mapfzcons1  26794  eldioph4b  26894  dnnumch3lem  27143  dnnumch3  27144  dgraalem  27350  dgraaub  27353  symgsssg  27408  symgfisg  27409  rabexgf  27695  relopabVD  28677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator