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

Theorem sseqtri 3670
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 3663 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 220 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sseqtr4i  3671  eqimssi  3692  abssi  3710  ssun2  3810  unixpss  5267  0ima  5517  idssxp  6047  fvssunirn  6255  mptexgf  6526  difex2  7011  oelim2  7720  omopthlem2  7781  sbthlem7  8117  unifpw  8310  fiuni  8375  rankuni  8764  rankc2  8772  rankxpu  8777  rankmapu  8779  rankxplim  8780  infxpenlem  8874  cf0  9111  fin23lem17  9198  fin23lem31  9203  smobeth  9446  nqerf  9790  dmrecnq  9828  ackbijnn  14604  divalglem2  15165  divalglem5  15167  bitsfzolem  15203  0bits  15208  bezoutlem2  15304  bezoutlem3  15305  lcmcllem  15356  lcmledvds  15359  lcmfval  15381  lcmfcllem  15385  lcmfledvds  15392  odzcllem  15544  odzdvds  15547  unbenlem  15659  4sqlem13  15708  4sqlem14  15709  4sqlem17  15712  4sqlem18  15713  vdwlem8  15739  vdwnnlem3  15748  ramcl2lem  15760  ramtcl  15761  ramtub  15763  strle1  16020  prdsval  16162  xpsc0  16267  xpsc1  16268  wunfunc  16606  wunnat  16663  psssdm2  17262  tsrss  17270  gicer  17765  symgsssg  17933  symgfisg  17934  odlem2  18004  gexlem2  18043  torsubg  18303  dprd2da  18487  zringlpirlem2  19881  zringlpirlem3  19882  pjfval  20098  pjpm  20100  toponsspwpw  20774  eltg4i  20812  ntrss2  20909  isopn3  20918  mretopd  20944  leordtval2  21064  ptbasfi  21432  hmphtop  21629  hmpher  21635  restutop  22088  ucnprima  22133  tngtopn  22501  tgioo  22646  xrtgioo  22656  ovolicc2lem4  23334  nulmbl2  23350  iundisj  23362  dyadmax  23412  i1f1  23502  dvfval  23706  dvcnp2  23728  lhop1lem  23821  lhop2  23823  elqaalem1  24119  elqaalem3  24121  taylthlem2  24173  pserulm  24221  psercn2  24222  psercnlem2  24223  psercnlem1  24224  psercn  24225  pserdvlem1  24226  pserdvlem2  24227  pserdv  24228  pserdv2  24229  abelth  24240  dvlog  24442  efopnlem2  24448  logtayl  24451  cxpcn3lem  24533  cxpcn3  24534  resqrtcn  24535  dvatan  24707  atancn  24708  rlimcnp  24737  rlimcnp2  24738  wilthlem3  24841  ftalem4  24847  ftalem5  24848  dchrisum0lem2a  25251  cchhllem  25812  axlowdimlem6  25872  hhssabloilem  28246  choc1  28314  chub2i  28457  span0  28529  spanuni  28531  sshhococi  28533  chsup0  28535  spansnpji  28565  mayetes3i  28716  nlelshi  29047  pjimai  29163  pj3i  29195  shatomistici  29348  hatomistici  29349  atcvat4i  29384  iundisjf  29528  rinvf1o  29560  mptctf  29623  iundisjfi  29683  xrge0mulgnn0  29817  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  esumcvgsum  30278  coinfliprv  30672  signsply0  30756  signstcl  30770  signstf  30771  kur14lem6  31319  mthmsta  31601  bdayimaon  31968  nosupbday  31976  noetalem3  31990  noetalem4  31991  nocvxminlem  32018  nocvxmin  32019  filnetlem3  32500  filnetlem4  32501  onint1  32573  oninhaus  32574  bj-nuliotaALT  33145  imadifss  33514  poimirlem3  33542  poimirlem32  33571  dvtan  33590  itg2addnclem2  33592  ftc1anclem6  33620  heiborlem3  33742  isdrngo2  33887  elrfi  37574  mapfzcons1  37597  eldioph4b  37692  dnnumch3lem  37933  dnnumch3  37934  dgraalem  38032  dgraaub  38035  resnonrel  38215  rtrclex  38241  rtrclexi  38245  cotrcltrcl  38334  cotrclrcl  38351  frege131d  38373  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  relopabVD  39451  rabexgf  39497  fzssnn0  39846  iuneqfzuzlem  39863  allbutfiinf  39960  uzublem  39970  sumnnodd  40180  lptioo2cn  40195  lptioo1cn  40196  fourierdlem31  40673  fourierdlem102  40743  fourierdlem114  40755  fouriercn  40767  elaa2lem  40768  etransclem48  40817  salexct  40870  salgencntex  40879  sge0resplit  40941  meaiuninclem  41015  caratheodorylem1  41061  hoicvr  41083  hoicvrrex  41091  hoidmvlelem3  41132  hoidmvlelem4  41133
  Copyright terms: Public domain W3C validator