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

Theorem sseqtr4i 3341
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 2408 . 2  |-  B  =  C
41, 3sseqtri 3340 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    C_ wss 3280
This theorem is referenced by:  eqimss2i  3363  snsspr1  3907  snsspr2  3908  snsstp1  3909  snsstp2  3910  snsstp3  3911  unissint  4034  iunxdif2  4099  intabs  4321  sssucid  4618  opabssxp  4909  dmresi  5155  cnvimass  5183  ssrnres  5268  sofld  5277  cnvcnv  5282  cnvssrndm  5350  fvclss  5939  dmmpt2ssx  6375  tfrlem11  6608  oawordeulem  6756  mapex  6983  trcl  7620  dfac3  7958  cfsuc  8093  fin23lem11  8153  domtriomlem  8278  ttukeylem1  8345  ttukeylem7  8351  brdom7disj  8365  brdom6disj  8366  fingch  8454  fpwwe2lem13  8473  canthp1lem2  8484  wunex2  8569  wunex3  8572  ressxr  9085  ltrelxr  9095  nnssnn0  10180  un0addcl  10209  un0mulcl  10210  caubnd  12117  isumclim3  12498  znnen  12767  isprm3  13043  phimullem  13123  vdwnnlem1  13318  isstruct2  13433  2strbas  13521  2strop  13522  rngbase  13532  rngplusg  13533  rngmulr  13534  srngbase  13540  srngplusg  13541  srngmulr  13542  srnginvl  13543  lmodbase  13549  lmodplusg  13550  lmodsca  13551  lmodvsca  13552  algbase  13554  algaddg  13555  algmulr  13556  algsca  13557  algvsca  13558  phlbase  13564  phlplusg  13565  phlsca  13566  phlvsca  13567  phlip  13568  topgrpbas  13572  topgrpplusg  13573  topgrptset  13574  otpsbas  13579  otpstset  13580  otpsle  13581  odrngbas  13590  odrngplusg  13591  odrngmulr  13592  odrngtset  13593  odrngle  13594  odrngds  13595  homarw  14156  ipoval  14535  ipolerval  14537  cycsubg  14923  eqgfval  14943  gsumval3  15469  gsumzaddlem  15481  islbs3  16182  cnfldbas  16662  cnfldadd  16663  cnfldmul  16664  cnfldcj  16665  cnfldtset  16666  cnfldle  16667  cnfldds  16668  cnfldunif  16669  basdif0  16973  tgdif0  17012  iscldtop  17114  iocpnfordt  17233  icomnfordt  17234  iooordt  17235  cnrest2  17304  cmpcov2  17407  fiuncmp  17421  indiscon  17434  xkococnlem  17644  hmphdis  17781  uzrest  17882  ufildr  17916  fin1aufil  17917  eltsms  18115  ustval  18185  qtopbaslem  18745  tgqioo  18784  re2ndc  18785  xrhmeo  18924  bndth  18936  pi1xfrcnvlem  19034  ovolficcss  19319  nulmbl2  19384  uniiccdif  19423  opnmbllem  19446  opnmblALT  19448  mbfimaopnlem  19500  i1fima  19523  i1fima2  19524  i1fd  19526  c1liplem1  19833  deg1n0ima  19965  efcvx  20318  dvrelog  20481  dvloglem  20492  logf1o2  20494  dvlog  20495  ressatans  20727  wilthlem3  20806  ex-ss  21688  ajfval  22263  ipasslem8  22291  hlimcaui  22692  shsspwh  22701  hhssabloi  22715  hhssnv  22717  hhshsslem1  22720  shunssji  22824  sshhococi  23001  pjoml6i  23044  osumcori  23098  mayete3i  23183  mayete3iOLD  23184  mayetes3i  23185  imaelshi  23514  pjclem1  23651  pjci  23656  mdcompli  23885  dmdcompli  23886  xppreima  24012  fzssnn  24100  rnlogblem  24352  esumpcvgval  24421  esumcvg  24429  elmbfmvol2  24570  sxbrsigalem0  24574  ballotlemsup  24715  ballotlem7  24746  subfacp1lem2a  24819  subfacp1lem2b  24820  erdszelem2  24831  kur14lem7  24851  kur14lem9  24853  fprodefsum  25251  iprodclim3  25266  dfon2lem2  25354  wfrlem14  25483  bpoly4  26009  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  volsupnfl  26150  locfincmp  26274  sdclem2  26336  heibor1lem  26408  ismrc  26645  mapfzcons1cl  26664  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  rabdiophlem2  26752  jm2.27dlem5  26974  lhe4.4ex1a  27414  dvcosre  27608  bnj931  28847  bnj1137  29070  dicval  31659  dvhdimlem  31927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator