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

Theorem sseqtri 3954
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
Hypotheses
Ref Expression
sseqtr.1 𝐴𝐵
sseqtr.2 𝐵 = 𝐶
Assertion
Ref Expression
sseqtri 𝐴𝐶

Proof of Theorem sseqtri
StepHypRef Expression
1 sseqtr.1 . 2 𝐴𝐵
2 sseqtr.2 . . 3 𝐵 = 𝐶
32sseq2i 3947 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 233 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  sseqtrri  3955  eqimssi  3976  abssi  4000  ssun2  4103  unixpss  5651  0ima  5917  fvssunirn  6678  mptexgf  6966  difex2  7466  oelim2  8208  omopthlem2  8270  sbthlem7  8621  unifpw  8815  fiuni  8880  rankuni  9280  rankc2  9288  rankxpu  9293  rankmapu  9295  rankxplim  9296  infxpenlem  9428  cf0  9666  fin23lem17  9753  fin23lem31  9758  smobeth  10001  nqerf  10345  dmrecnq  10383  ackbijnn  15178  divalglem2  15739  divalglem5  15741  bitsfzolem  15776  0bits  15781  bezoutlem2  15881  bezoutlem3  15882  lcmcllem  15933  lcmledvds  15936  lcmfval  15958  lcmfcllem  15962  lcmfledvds  15969  odzcllem  16122  odzdvds  16125  unbenlem  16237  4sqlem13  16286  4sqlem14  16287  4sqlem17  16290  4sqlem18  16291  vdwlem8  16317  vdwnnlem3  16326  ramcl2lem  16338  ramtcl  16339  ramtub  16341  strle1  16587  prdsval  16723  wunfunc  17164  wunnat  17221  psssdm2  17820  tsrss  17828  gicer  18411  symgsssg  18590  symgfisg  18591  odfval  18655  odlem2  18662  gexlem2  18702  torsubg  18970  dprd2da  19160  zringlpirlem2  20181  zringlpirlem3  20182  pjfval  20398  pjpm  20400  toponsspwpw  21530  eltg4i  21568  ntrss2  21665  isopn3  21674  mretopd  21700  leordtval2  21820  ptbasfi  22189  hmphtop  22386  hmpher  22392  restutop  22846  ucnprima  22891  tngtopn  23259  tgioo  23404  xrtgioo  23414  ovolicc2lem4  24127  nulmbl2  24143  iundisj  24155  dyadmax  24205  i1f1  24297  dvfval  24503  dvcnp2  24526  lhop1lem  24619  lhop2  24621  elqaalem1  24918  elqaalem3  24920  taylthlem2  24972  pserulm  25020  psercn2  25021  psercnlem2  25022  psercnlem1  25023  psercn  25024  pserdvlem1  25025  pserdvlem2  25026  pserdv  25027  pserdv2  25028  abelth  25039  dvlog  25245  efopnlem2  25251  logtayl  25254  cxpcn3lem  25339  cxpcn3  25340  resqrtcn  25341  dvatan  25524  atancn  25525  rlimcnp  25554  rlimcnp2  25555  wilthlem3  25658  ftalem4  25664  ftalem5  25665  dchrisum0lem2a  26104  cchhllem  26684  axlowdimlem6  26744  hhssabloilem  29047  choc1  29113  chub2i  29256  span0  29328  spanuni  29330  sshhococi  29332  chsup0  29334  spansnpji  29364  mayetes3i  29515  nlelshi  29846  pjimai  29962  pj3i  29994  shatomistici  30147  hatomistici  30148  atcvat4i  30183  iundisjf  30355  rinvf1o  30392  mptctf  30482  iundisjfi  30548  xrge0mulgnn0  30726  gsumpart  30743  ccfldsrarelvec  31144  ccfldextdgrr  31145  xrge0iifcnv  31284  xrge0iifiso  31286  xrge0iifhom  31288  esumcvgsum  31455  coinfliprv  31848  signsply0  31929  signstcl  31943  signstf  31944  kur14lem6  32566  mthmsta  32933  bdayimaon  33305  nosupbday  33313  noetalem3  33327  noetalem4  33328  nocvxminlem  33355  nocvxmin  33356  filnetlem3  33836  filnetlem4  33837  onint1  33905  oninhaus  33906  bj-nuliotaALT  34470  imadifss  35025  poimirlem3  35053  poimirlem32  35082  dvtan  35100  itg2addnclem2  35102  ftc1anclem6  35128  heiborlem3  35244  isdrngo2  35389  elrfi  39622  mapfzcons1  39645  eldioph4b  39739  dnnumch3lem  39977  dnnumch3  39978  dgraalem  40076  dgraaub  40079  resnonrel  40279  cotrcltrcl  40413  cotrclrcl  40430  frege131d  40452  binomcxplemdvbinom  41044  binomcxplemdvsum  41046  binomcxplemnotnn0  41047  relopabVD  41594  rabexgf  41640  fzssnn0  41936  iuneqfzuzlem  41953  allbutfiinf  42044  uzublem  42054  sumnnodd  42259  lptioo2cn  42274  lptioo1cn  42275  fourierdlem31  42767  fourierdlem102  42837  fourierdlem114  42849  fouriercn  42861  elaa2lem  42862  etransclem48  42911  salexct  42961  salgencntex  42970  sge0resplit  43032  meaiuninclem  43106  caratheodorylem1  43152  hoicvr  43174  hoicvrrex  43182  hoidmvlelem3  43223  hoidmvlelem4  43224
  Copyright terms: Public domain W3C validator