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

Theorem sseqtr4i 3224
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtr4.1  |-  A  C_  B
sseqtr4.2  |-  C  =  B
Assertion
Ref Expression
sseqtr4i  |-  A  C_  C

Proof of Theorem sseqtr4i
StepHypRef Expression
1 sseqtr4.1 . 2  |-  A  C_  B
2 sseqtr4.2 . . 3  |-  C  =  B
32eqcomi 2300 . 2  |-  B  =  C
41, 3sseqtri 3223 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    C_ wss 3165
This theorem is referenced by:  eqimss2i  3246  snsspr1  3780  snsspr2  3781  snsstp1  3782  snsstp2  3783  snsstp3  3784  unissint  3902  iunxdif2  3966  intabs  4188  sssucid  4485  opabssxp  4778  dmresi  5021  cnvimass  5049  ssrnres  5132  sofld  5137  cnvcnv  5142  cnvssrndm  5210  fvclss  5776  dmmpt2ssx  6205  tfrlem11  6420  oawordeulem  6568  mapex  6794  trcl  7426  dfac3  7764  cfsuc  7899  fin23lem11  7959  domtriomlem  8084  ttukeylem1  8152  ttukeylem7  8158  brdom7disj  8172  brdom6disj  8173  fingch  8261  fpwwe2lem13  8280  canthp1lem2  8291  wunex2  8376  wunex3  8379  ressxr  8892  ltrelxr  8902  nnssnn0  9984  un0addcl  10013  un0mulcl  10014  caubnd  11858  isumclim3  12238  znnen  12507  isprm3  12783  phimullem  12863  vdwnnlem1  13058  isstruct2  13173  2strbas  13261  2strop  13262  rngbase  13272  rngplusg  13273  rngmulr  13274  srngbase  13280  srngplusg  13281  srngmulr  13282  srnginvl  13283  lmodbase  13289  lmodplusg  13290  lmodsca  13291  lmodvsca  13292  algbase  13294  algaddg  13295  algmulr  13296  algsca  13297  algvsca  13298  phlbase  13304  phlplusg  13305  phlsca  13306  phlvsca  13307  phlip  13308  topgrpbas  13312  topgrpplusg  13313  topgrptset  13314  otpsbas  13319  otpstset  13320  otpsle  13321  odrngbas  13328  odrngplusg  13329  odrngmulr  13330  odrngtset  13331  odrngle  13332  odrngds  13333  homarw  13894  ipoval  14273  ipolerval  14275  cycsubg  14661  eqgfval  14681  gsumval3  15207  gsumzaddlem  15219  islbs3  15924  cnfldbas  16399  cnfldadd  16400  cnfldmul  16401  cnfldcj  16402  cnfldtset  16403  cnfldle  16404  cnfldds  16405  basdif0  16707  tgdif0  16746  iscldtop  16848  iocpnfordt  16961  icomnfordt  16962  iooordt  16963  cnrest2  17030  cmpcov2  17133  fiuncmp  17147  indiscon  17160  xkococnlem  17369  hmphdis  17503  uzrest  17608  ufildr  17642  fin1aufil  17643  eltsms  17831  qtopbaslem  18283  tgqioo  18322  re2ndc  18323  xrhmeo  18460  bndth  18472  pi1xfrcnvlem  18570  ovolficcss  18845  nulmbl2  18910  uniiccdif  18949  opnmbllem  18972  opnmblALT  18974  mbfimaopnlem  19026  i1fima  19049  i1fima2  19050  i1fd  19052  c1liplem1  19359  deg1n0ima  19491  efcvx  19841  dvrelog  20000  dvloglem  20011  logf1o2  20013  dvlog  20014  ressatans  20246  wilthlem3  20324  ex-ss  20830  ajfval  21403  ipasslem8  21431  hlimcaui  21832  shsspwh  21841  hhssabloi  21855  hhssnv  21857  hhshsslem1  21860  shunssji  21964  sshhococi  22141  pjoml6i  22184  osumcori  22238  mayete3i  22323  mayete3iOLD  22324  mayetes3i  22325  imaelshi  22654  pjclem1  22791  pjci  22796  mdcompli  23025  dmdcompli  23026  ballotlemsup  23079  ballotlem7  23110  xppreima  23226  fzssnn  23291  rnlogblem  23416  esumpcvgval  23461  esumcvg  23469  elmbfmvol2  23587  subfacp1lem2a  23726  subfacp1lem2b  23727  erdszelem2  23738  kur14lem7  23758  kur14lem9  23760  dfon2lem2  24211  wfrlem14  24340  bpoly4  24866  residcp  25180  imfstnrelc  25184  pvp  26151  pgapspf  26155  locfincmp  26407  sdclem2  26555  heibor1lem  26636  ismrc  26879  mapfzcons1cl  26898  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  rabdiophlem2  26986  jm2.27dlem5  27209  lhe4.4ex1a  27649  dvcosre  27844  bnj931  29118  bnj1137  29341  dicval  31988  dvhdimlem  32256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator