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

Theorem sseqtri 3600
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 3593 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 219 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  sseqtr4i  3601  eqimssi  3622  abssi  3640  ssun2  3739  unixpss  5157  0ima  5401  fvssunirn  6127  difex2  6863  oelim2  7562  omopthlem2  7623  sbthlem7  7961  unifpw  8152  fiuni  8217  rankuni  8609  rankc2  8617  rankxpu  8622  rankmapu  8624  rankxplim  8625  infxpenlem  8719  cf0  8956  fin23lem17  9043  fin23lem31  9048  smobeth  9287  nqerf  9631  dmrecnq  9669  ackbijnn  14399  divalglem2  14956  divalglem5  14958  bitsfzolem  14994  0bits  14999  bezoutlem2  15095  bezoutlem3  15096  lcmcllem  15147  lcmledvds  15150  lcmfval  15172  lcmfcllem  15176  lcmfledvds  15183  odzcllem  15335  odzdvds  15338  unbenlem  15450  4sqlem13  15499  4sqlem14  15500  4sqlem17  15503  4sqlem18  15504  vdwlem8  15530  vdwnnlem3  15539  ramcl2lem  15551  ramtcl  15552  ramtub  15554  strle1  15800  prdsval  15938  xpsc0  16043  xpsc1  16044  wunfunc  16382  wunnat  16439  psssdm2  17038  tsrss  17046  gicer  17541  gicerOLD  17542  symgsssg  17710  symgfisg  17711  odlem2  17781  gexlem2  17820  torsubg  18080  dprd2da  18264  zringlpirlem2  19652  zringlpirlem3  19653  pjfval  19869  pjpm  19871  eltg4i  20575  ntrss2  20671  isopn3  20680  mretopd  20706  leordtval2  20826  ptbasfi  21194  hmphtop  21391  hmpher  21397  restutop  21851  ucnprima  21896  tngtopn  22264  tgioo  22407  xrtgioo  22417  ovolicc2lem4  23095  nulmbl2  23111  iundisj  23123  dyadmax  23172  i1f1  23263  dvfval  23467  dvcnp2  23489  lhop1lem  23580  lhop2  23582  elqaalem1  23878  elqaalem3  23880  taylthlem2  23932  pserulm  23980  psercn2  23981  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  pserdv  23987  pserdv2  23988  abelth  23999  dvlog  24197  efopnlem2  24203  logtayl  24206  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  dvatan  24462  atancn  24463  rlimcnp  24492  rlimcnp2  24493  wilthlem3  24596  ftalem4  24602  ftalem5  24603  dchrisum0lem2a  25006  cchhllem  25567  axlowdimlem6  25627  hhssabloilem  27502  choc1  27570  chub2i  27713  span0  27785  spanuni  27787  sshhococi  27789  chsup0  27791  spansnpji  27821  mayetes3i  27972  nlelshi  28303  pjimai  28419  pj3i  28451  shatomistici  28604  hatomistici  28605  atcvat4i  28640  iundisjf  28784  mptexgf  28809  idssxp  28811  rinvf1o  28814  mptctf  28883  iundisjfi  28942  xrge0mulgnn0  29020  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  esumcvgsum  29477  coinfliprv  29871  signsply0  29954  signstcl  29968  signstf  29969  kur14lem6  30447  mthmsta  30729  nocvxminlem  31089  nocvxmin  31090  nobndlem1  31091  nobndlem2  31092  filnetlem3  31545  filnetlem4  31546  onint1  31618  oninhaus  31619  bj-nuliotaALT  32211  bj-sspwpweq  32240  bj-toponss  32241  imadifss  32554  poimirlem3  32582  poimirlem32  32611  dvtan  32630  itg2addnclem2  32632  ftc1anclem6  32660  heiborlem3  32782  isdrngo2  32927  elrfi  36275  mapfzcons1  36298  eldioph4b  36393  dnnumch3lem  36634  dnnumch3  36635  dgraalem  36734  dgraaub  36737  resnonrel  36917  rtrclex  36943  rtrclexi  36947  cotrcltrcl  37036  cotrclrcl  37053  frege131d  37075  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  relopabVD  38159  rabexgf  38206  fzssnn0  38474  iuneqfzuzlem  38491  sumnnodd  38697  lptioo2cn  38712  lptioo1cn  38713  fourierdlem31  39031  fourierdlem102  39101  fourierdlem114  39113  fouriercn  39125  elaa2lem  39126  etransclem48  39175  salexct  39228  salgencntex  39237  sge0resplit  39299  meaiuninclem  39373  caratheodorylem1  39416  hoicvr  39438  hoicvrrex  39446  hoidmvlelem3  39487  hoidmvlelem4  39488
  Copyright terms: Public domain W3C validator