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

Theorem sseqtri 3474
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 3467 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3421  df-ss 3428
This theorem is referenced by:  sseqtr4i  3475  eqimssi  3496  abssi  3514  ssun2  3607  unixpss  4938  0ima  5173  fvssunirn  5872  difex2  6589  oelim2  7281  omopthlem2  7342  sbthlem7  7671  unifpw  7857  fiuni  7922  rankuni  8313  rankc2  8321  rankxpu  8326  rankmapu  8328  rankxplim  8329  infxpenlem  8423  cf0  8663  fin23lem17  8750  fin23lem31  8755  smobeth  8993  nqerf  9338  dmrecnq  9376  ackbijnn  13791  divalglem2  14262  divalglem5  14264  bitsfzolem  14293  0bits  14298  bezoutlem2  14386  bezoutlem3  14387  odzcllem  14528  odzdvds  14531  unbenlem  14635  4sqlem13  14684  4sqlem14  14685  4sqlem17  14688  4sqlem18  14689  vdwlem8  14715  vdwnnlem3  14724  ramcl2lem  14736  ramtcl  14737  ramtub  14739  strle1  14940  prdsval  15069  xpsc0  15174  xpsc1  15175  wunfunc  15512  wunnat  15569  psssdm2  16169  tsrss  16177  gicer  16648  symgsssg  16816  symgfisg  16817  odlem2  16887  gexlem2  16926  torsubg  17184  gsumzaddlemOLD  17260  dprd2da  17411  zringlpirlem2  18823  zringlpirlem3  18824  pjfval  19035  pjpm  19037  eltg4i  19753  ntrss2  19850  isopn3  19860  mretopd  19886  leordtval2  20006  ptbasfi  20374  hmphtop  20571  hmpher  20577  restutop  21032  ucnprima  21077  tngtopn  21456  tgioo  21593  xrtgioo  21603  ovolicc2lem4  22223  nulmbl2  22239  iundisj  22250  dyadmax  22299  i1f1  22389  dvfval  22593  dvcnp2  22615  lhop1lem  22706  lhop2  22708  elqaalem1  23007  elqaalem3  23009  taylthlem2  23061  pserulm  23109  psercn2  23110  psercnlem2  23111  psercnlem1  23112  psercn  23113  pserdvlem1  23114  pserdvlem2  23115  pserdv  23116  pserdv2  23117  abelth  23128  dvlog  23326  efopnlem2  23332  logtayl  23335  cxpcn3lem  23417  cxpcn3  23418  resqrtcn  23419  dvatan  23591  atancn  23592  rlimcnp  23621  rlimcnp2  23622  wilthlem3  23725  ftalem4  23730  ftalem5  23731  dchrisum0lem2a  24083  cchhllem  24607  axlowdimlem6  24667  choc1  26659  chub2i  26802  span0  26874  spanuni  26876  sshhococi  26878  chsup0  26880  spansnpji  26910  mayetes3i  27061  nlelshi  27392  pjimai  27508  pj3i  27540  shatomistici  27693  hatomistici  27694  atcvat4i  27729  iundisjf  27881  mptexgf  27908  idssxp  27910  rinvf1o  27913  mptctf  27990  iundisjfi  28049  xrge0mulgnn0  28129  xrge0iifcnv  28368  xrge0iifiso  28370  xrge0iifhom  28372  esumcvgsum  28535  coinfliprv  28927  signsply0  29014  signstcl  29028  signstf  29029  kur14lem6  29508  mthmsta  29790  nocvxminlem  30150  nocvxmin  30151  nobndlem1  30152  nobndlem2  30153  filnetlem3  30608  filnetlem4  30609  onint1  30681  oninhaus  30682  bj-nuliotaALT  31152  dvtan  31438  itg2addnclem2  31440  ftc1anclem6  31468  heiborlem3  31591  isdrngo2  31643  elrfi  34988  mapfzcons1  35011  eldioph4b  35106  dnnumch3lem  35354  dnnumch3  35355  dgraalem  35458  dgraaub  35461  cotrcltrcl  35704  cotrclrcl  35721  frege131d  35743  lcmcllem  36050  lcmledvds  36053  binomcxplemdvbinom  36106  binomcxplemdvsum  36108  binomcxplemnotnn0  36109  relopabVD  36732  rabexgf  36779  fzssnn0  36891  sumnnodd  37004  lptioo2cn  37019  lptioo1cn  37020  fourierdlem31  37288  fourierdlem102  37359  fourierdlem114  37371  fouriercn  37383  elaa2lem  37384  etransclem48  37433
  Copyright terms: Public domain W3C validator