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

Theorem sseqtr4i 3377
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 2437 . 2  |-  B  =  C
41, 3sseqtri 3376 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  eqimss2i  3399  snsspr1  4010  snsspr2  4011  snsstp1  4012  snsstp2  4013  snsstp3  4014  unissint  4140  iunxdif2  4206  intabs  4441  sssucid  4783  opabssxp  4898  dmresi  5149  cnvimass  5177  ssrnres  5264  sofld  5274  cnvcnv  5278  cnvssrndm  5347  fvclss  5946  dmmpt2ssx  6628  suppun  6698  tfrlem11  6833  oawordeulem  6981  mapex  7208  trcl  7936  dfac3  8279  cfsuc  8414  fin23lem11  8474  domtriomlem  8599  ttukeylem1  8666  ttukeylem7  8672  brdom7disj  8686  brdom6disj  8687  fingch  8778  fpwwe2lem13  8797  canthp1lem2  8808  wunex2  8893  wunex3  8896  ressxr  9415  ltrelxr  9426  nnssnn0  10570  un0addcl  10601  un0mulcl  10602  fzossnn0  11564  caubnd  12830  isumclim3  13210  znnen  13478  isprm3  13755  phimullem  13837  vdwnnlem1  14039  isstruct2  14166  2strbas  14258  2strop  14259  rngbase  14269  rngplusg  14270  rngmulr  14271  srngbase  14277  srngplusg  14278  srngmulr  14279  srnginvl  14280  lmodbase  14286  lmodplusg  14287  lmodsca  14288  lmodvsca  14289  ipsbase  14293  ipsaddg  14294  ipsmulr  14295  ipssca  14296  ipsvsca  14297  ipsip  14298  phlbase  14303  phlplusg  14304  phlsca  14305  phlvsca  14306  phlip  14307  topgrpbas  14311  topgrpplusg  14312  topgrptset  14313  otpsbas  14318  otpstset  14319  otpsle  14320  odrngbas  14329  odrngplusg  14330  odrngmulr  14331  odrngtset  14332  odrngle  14333  odrngds  14334  homarw  14897  ipoval  15307  ipolerval  15309  cycsubg  15689  eqgfval  15709  gsumval3OLD  16362  gsumval3  16365  gsumzaddlemOLD  16390  islbs3  17158  cnfldbas  17666  cnfldadd  17667  cnfldmul  17668  cnfldcj  17669  cnfldtset  17670  cnfldle  17671  cnfldds  17672  cnfldunif  17673  basdif0  18400  tgdif0  18439  iscldtop  18541  iocpnfordt  18661  icomnfordt  18662  iooordt  18663  cnrest2  18732  cmpcov2  18835  fiuncmp  18849  bwth  18855  indiscon  18864  xkococnlem  19074  hmphdis  19211  uzrest  19312  ufildr  19346  fin1aufil  19347  eltsms  19545  ustval  19619  qtopbaslem  20179  tgqioo  20219  re2ndc  20220  xrhmeo  20360  bndth  20372  pi1xfrcnvlem  20470  ovolficcss  20795  nulmbl2  20860  uniiccdif  20900  opnmbllem  20923  opnmblALT  20925  mbfimaopnlem  20975  i1fima  20998  i1fima2  20999  i1fd  21001  c1liplem1  21310  deg1n0ima  21445  efcvx  21799  dvrelog  21967  dvloglem  21978  logf1o2  21980  dvlog  21981  ressatans  22214  wilthlem3  22293  trkgbas  22791  trkgdist  22792  trkgitv  22793  ex-ss  23457  ajfval  24032  ipasslem8  24060  hlimcaui  24462  shsspwh  24472  hhssabloi  24486  hhssnv  24488  hhshsslem1  24491  shunssji  24595  sshhococi  24772  pjoml6i  24815  osumcori  24869  mayete3i  24954  mayete3iOLD  24955  mayetes3i  24956  imaelshi  25285  pjclem1  25422  pjci  25427  mdcompli  25656  dmdcompli  25657  xppreima  25788  fzssnn  25897  gsummpt2co  26101  rnlogblem  26312  esumpcvgval  26381  esumcvg  26389  elmbfmvol2  26536  sxbrsigalem0  26540  eulerpartlemsv3  26592  ballotlemsup  26735  ballotlem7  26766  signswbase  26803  signswplusg  26804  subfacp1lem2a  26916  subfacp1lem2b  26917  erdszelem2  26928  kur14lem7  26948  kur14lem9  26950  fprodefsum  27332  iprodclim3  27347  dfon2lem2  27444  wfrlem14  27584  bpoly4  28049  opnmbllem0  28271  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  volsupnfl  28280  locfincmp  28420  sdclem2  28482  heibor1lem  28552  ismrc  28882  mapfzcons1cl  28899  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  rabdiophlem2  28985  jm2.27dlem5  29207  algbase  29380  algaddg  29381  algmulr  29382  algsca  29383  algvsca  29384  lhe4.4ex1a  29448  dvcosre  29634  dmmpt2ssx2  30571  bnj931  31466  bnj1137  31688  bj-snglsstag  32057  bj-2upln1upl  32100  bj-ccssccbar  32120  bj-ccinftyssccbar  32121  dicval  34394  dvhdimlem  34662
  Copyright terms: Public domain W3C validator