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

Theorem sseqtri 3622
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 3615 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 220 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  sseqtr4i  3623  eqimssi  3644  abssi  3662  ssun2  3761  unixpss  5205  0ima  5451  fvssunirn  6184  mptexgf  6450  difex2  6933  oelim2  7635  omopthlem2  7696  sbthlem7  8036  unifpw  8229  fiuni  8294  rankuni  8686  rankc2  8694  rankxpu  8699  rankmapu  8701  rankxplim  8702  infxpenlem  8796  cf0  9033  fin23lem17  9120  fin23lem31  9125  smobeth  9368  nqerf  9712  dmrecnq  9750  ackbijnn  14504  divalglem2  15061  divalglem5  15063  bitsfzolem  15099  0bits  15104  bezoutlem2  15200  bezoutlem3  15201  lcmcllem  15252  lcmledvds  15255  lcmfval  15277  lcmfcllem  15281  lcmfledvds  15288  odzcllem  15440  odzdvds  15443  unbenlem  15555  4sqlem13  15604  4sqlem14  15605  4sqlem17  15608  4sqlem18  15609  vdwlem8  15635  vdwnnlem3  15644  ramcl2lem  15656  ramtcl  15657  ramtub  15659  strle1  15913  prdsval  16055  xpsc0  16160  xpsc1  16161  wunfunc  16499  wunnat  16556  psssdm2  17155  tsrss  17163  gicer  17658  gicerOLD  17659  symgsssg  17827  symgfisg  17828  odlem2  17898  gexlem2  17937  torsubg  18197  dprd2da  18381  zringlpirlem2  19773  zringlpirlem3  19774  pjfval  19990  pjpm  19992  toponsspwpw  20666  eltg4i  20704  ntrss2  20801  isopn3  20810  mretopd  20836  leordtval2  20956  ptbasfi  21324  hmphtop  21521  hmpher  21527  restutop  21981  ucnprima  22026  tngtopn  22394  tgioo  22539  xrtgioo  22549  ovolicc2lem4  23228  nulmbl2  23244  iundisj  23256  dyadmax  23306  i1f1  23397  dvfval  23601  dvcnp2  23623  lhop1lem  23714  lhop2  23716  elqaalem1  24012  elqaalem3  24014  taylthlem2  24066  pserulm  24114  psercn2  24115  psercnlem2  24116  psercnlem1  24117  psercn  24118  pserdvlem1  24119  pserdvlem2  24120  pserdv  24121  pserdv2  24122  abelth  24133  dvlog  24331  efopnlem2  24337  logtayl  24340  cxpcn3lem  24422  cxpcn3  24423  resqrtcn  24424  dvatan  24596  atancn  24597  rlimcnp  24626  rlimcnp2  24627  wilthlem3  24730  ftalem4  24736  ftalem5  24737  dchrisum0lem2a  25140  cchhllem  25701  axlowdimlem6  25761  hhssabloilem  28006  choc1  28074  chub2i  28217  span0  28289  spanuni  28291  sshhococi  28293  chsup0  28295  spansnpji  28325  mayetes3i  28476  nlelshi  28807  pjimai  28923  pj3i  28955  shatomistici  29108  hatomistici  29109  atcvat4i  29144  iundisjf  29288  idssxp  29314  rinvf1o  29317  mptctf  29379  iundisjfi  29438  xrge0mulgnn0  29516  xrge0iifcnv  29803  xrge0iifiso  29805  xrge0iifhom  29807  esumcvgsum  29973  coinfliprv  30367  signsply0  30450  signstcl  30464  signstf  30465  kur14lem6  30954  mthmsta  31236  nocvxminlem  31606  nocvxmin  31607  nobndlem1  31608  nobndlem2  31609  filnetlem3  32070  filnetlem4  32071  onint1  32143  oninhaus  32144  bj-nuliotaALT  32720  imadifss  33055  poimirlem3  33083  poimirlem32  33112  dvtan  33131  itg2addnclem2  33133  ftc1anclem6  33161  heiborlem3  33283  isdrngo2  33428  elrfi  36776  mapfzcons1  36799  eldioph4b  36894  dnnumch3lem  37135  dnnumch3  37136  dgraalem  37235  dgraaub  37238  resnonrel  37418  rtrclex  37444  rtrclexi  37448  cotrcltrcl  37537  cotrclrcl  37554  frege131d  37576  binomcxplemdvbinom  38073  binomcxplemdvsum  38075  binomcxplemnotnn0  38076  relopabVD  38659  rabexgf  38705  fzssnn0  39032  iuneqfzuzlem  39049  allbutfiinf  39146  uzublem  39156  sumnnodd  39298  lptioo2cn  39313  lptioo1cn  39314  fourierdlem31  39692  fourierdlem102  39762  fourierdlem114  39774  fouriercn  39786  elaa2lem  39787  etransclem48  39836  salexct  39889  salgencntex  39898  sge0resplit  39960  meaiuninclem  40034  caratheodorylem1  40077  hoicvr  40099  hoicvrrex  40107  hoidmvlelem3  40148  hoidmvlelem4  40149
  Copyright terms: Public domain W3C validator