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

Theorem sseqtr4i 3373
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 2439 . 2  |-  B  =  C
41, 3sseqtri 3372 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312
This theorem is referenced by:  eqimss2i  3395  snsspr1  3939  snsspr2  3940  snsstp1  3941  snsstp2  3942  snsstp3  3943  unissint  4066  iunxdif2  4131  intabs  4353  sssucid  4650  opabssxp  4942  dmresi  5188  cnvimass  5216  ssrnres  5301  sofld  5310  cnvcnv  5315  cnvssrndm  5383  fvclss  5972  dmmpt2ssx  6408  tfrlem11  6641  oawordeulem  6789  mapex  7016  trcl  7656  dfac3  7994  cfsuc  8129  fin23lem11  8189  domtriomlem  8314  ttukeylem1  8381  ttukeylem7  8387  brdom7disj  8401  brdom6disj  8402  fingch  8490  fpwwe2lem13  8509  canthp1lem2  8520  wunex2  8605  wunex3  8608  ressxr  9121  ltrelxr  9131  nnssnn0  10216  un0addcl  10245  un0mulcl  10246  caubnd  12154  isumclim3  12535  znnen  12804  isprm3  13080  phimullem  13160  vdwnnlem1  13355  isstruct2  13470  2strbas  13558  2strop  13559  rngbase  13569  rngplusg  13570  rngmulr  13571  srngbase  13577  srngplusg  13578  srngmulr  13579  srnginvl  13580  lmodbase  13586  lmodplusg  13587  lmodsca  13588  lmodvsca  13589  algbase  13591  algaddg  13592  algmulr  13593  algsca  13594  algvsca  13595  phlbase  13601  phlplusg  13602  phlsca  13603  phlvsca  13604  phlip  13605  topgrpbas  13609  topgrpplusg  13610  topgrptset  13611  otpsbas  13616  otpstset  13617  otpsle  13618  odrngbas  13627  odrngplusg  13628  odrngmulr  13629  odrngtset  13630  odrngle  13631  odrngds  13632  homarw  14193  ipoval  14572  ipolerval  14574  cycsubg  14960  eqgfval  14980  gsumval3  15506  gsumzaddlem  15518  islbs3  16219  cnfldbas  16699  cnfldadd  16700  cnfldmul  16701  cnfldcj  16702  cnfldtset  16703  cnfldle  16704  cnfldds  16705  cnfldunif  16706  basdif0  17010  tgdif0  17049  iscldtop  17151  iocpnfordt  17271  icomnfordt  17272  iooordt  17273  cnrest2  17342  cmpcov2  17445  fiuncmp  17459  indiscon  17473  xkococnlem  17683  hmphdis  17820  uzrest  17921  ufildr  17955  fin1aufil  17956  eltsms  18154  ustval  18224  qtopbaslem  18784  tgqioo  18823  re2ndc  18824  xrhmeo  18963  bndth  18975  pi1xfrcnvlem  19073  ovolficcss  19358  nulmbl2  19423  uniiccdif  19462  opnmbllem  19485  opnmblALT  19487  mbfimaopnlem  19539  i1fima  19562  i1fima2  19563  i1fd  19565  c1liplem1  19872  deg1n0ima  20004  efcvx  20357  dvrelog  20520  dvloglem  20531  logf1o2  20533  dvlog  20534  ressatans  20766  wilthlem3  20845  ex-ss  21727  ajfval  22302  ipasslem8  22330  hlimcaui  22731  shsspwh  22740  hhssabloi  22754  hhssnv  22756  hhshsslem1  22759  shunssji  22863  sshhococi  23040  pjoml6i  23083  osumcori  23137  mayete3i  23222  mayete3iOLD  23223  mayetes3i  23224  imaelshi  23553  pjclem1  23690  pjci  23695  mdcompli  23924  dmdcompli  23925  xppreima  24051  fzssnn  24139  rnlogblem  24391  esumpcvgval  24460  esumcvg  24468  elmbfmvol2  24609  sxbrsigalem0  24613  ballotlemsup  24754  ballotlem7  24785  subfacp1lem2a  24858  subfacp1lem2b  24859  erdszelem2  24870  kur14lem7  24890  kur14lem9  24892  fprodefsum  25290  iprodclim3  25305  dfon2lem2  25403  wfrlem14  25543  bpoly4  26097  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  volsupnfl  26241  locfincmp  26375  sdclem2  26437  heibor1lem  26509  ismrc  26746  mapfzcons1cl  26765  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  rabdiophlem2  26853  jm2.27dlem5  27075  lhe4.4ex1a  27514  dvcosre  27708  fzossnn0  28107  bnj931  29078  bnj1137  29301  dicval  31911  dvhdimlem  32179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator