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

Theorem sseqtr4i 3532
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 2470 . 2  |-  B  =  C
41, 3sseqtri 3531 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485
This theorem is referenced by:  eqimss2i  3554  snsspr1  4181  snsspr2  4182  snsstp1  4183  snsstp2  4184  snsstp3  4185  unissint  4313  iunxdif2  4380  intabs  4617  sssucid  4964  opabssxp  5083  dmresi  5339  cnvimass  5367  ssrnres  5452  sofld  5461  cnvcnv  5465  cnvssrndm  5535  fvclss  6155  dmmpt2ssx  6864  suppun  6938  tfrlem11  7075  oawordeulem  7221  mapex  7444  trcl  8176  dfac3  8519  cfsuc  8654  fin23lem11  8714  domtriomlem  8839  ttukeylem1  8906  ttukeylem7  8912  brdom7disj  8926  brdom6disj  8927  fingch  9018  fpwwe2lem13  9037  canthp1lem2  9048  wunex2  9133  wunex3  9136  ressxr  9654  ltrelxr  9665  nnssnn0  10819  un0addcl  10850  un0mulcl  10851  fzossnn0  11855  caubnd  13203  isumclim3  13586  iprodclim3  13805  fprodefsum  13842  znnen  13958  isprm3  14238  phimullem  14321  vdwnnlem1  14525  isstruct2  14653  2strbas  14753  2strop  14754  rngbase  14764  rngplusg  14765  rngmulr  14766  srngbase  14772  srngplusg  14773  srngmulr  14774  srnginvl  14775  lmodbase  14781  lmodplusg  14782  lmodsca  14783  lmodvsca  14784  ipsbase  14788  ipsaddg  14789  ipsmulr  14790  ipssca  14791  ipsvsca  14792  ipsip  14793  phlbase  14798  phlplusg  14799  phlsca  14800  phlvsca  14801  phlip  14802  topgrpbas  14806  topgrpplusg  14807  topgrptset  14808  otpsbas  14813  otpstset  14814  otpsle  14815  odrngbas  14824  odrngplusg  14825  odrngmulr  14826  odrngtset  14827  odrngle  14828  odrngds  14829  homarw  15452  ipoval  15911  ipolerval  15913  cycsubg  16356  eqgfval  16376  gsumval3OLD  17035  gsumval3  17038  gsumzaddlemOLD  17063  nn0gsumfz  17139  islbs3  17928  cnfldbas  18551  cnfldadd  18552  cnfldmul  18553  cnfldcj  18554  cnfldtset  18555  cnfldle  18556  cnfldds  18557  cnfldunif  18558  pmatcollpw3fi  19413  basdif0  19581  iscldtop  19723  iocpnfordt  19843  icomnfordt  19844  iooordt  19845  cnrest2  19914  cmpcov2  20017  fiuncmp  20031  bwth  20037  indiscon  20045  locfincmp  20153  xkococnlem  20286  hmphdis  20423  uzrest  20524  ufildr  20558  fin1aufil  20559  eltsms  20757  ustval  20831  qtopbaslem  21391  tgqioo  21431  re2ndc  21432  xrhmeo  21572  bndth  21584  pi1xfrcnvlem  21682  ovolficcss  22007  nulmbl2  22073  uniiccdif  22113  opnmbllem  22136  opnmblALT  22138  mbfimaopnlem  22188  i1fima  22211  i1fima2  22212  i1fd  22214  c1liplem1  22523  deg1n0ima  22615  efcvx  22970  dvrelog  23144  dvloglem  23155  logf1o2  23157  dvlog  23158  ressatans  23391  wilthlem3  23470  trkgbas  23967  trkgdist  23968  trkgitv  23969  ex-ss  25275  ajfval  25851  ipasslem8  25879  hlimcaui  26281  shsspwh  26291  hhssabloi  26305  hhssnv  26307  hhshsslem1  26310  shunssji  26414  sshhococi  26591  pjoml6i  26634  osumcori  26688  mayete3i  26773  mayete3iOLD  26774  mayetes3i  26775  imaelshi  27104  pjclem1  27241  pjci  27246  mdcompli  27475  dmdcompli  27476  xppreima  27635  fzssnn  27755  gsummpt2co  27931  circtopn  28001  esumpcvgval  28250  esumcvg  28258  elmbfmvol2  28411  sxbrsigalem0  28415  eulerpartlemsv3  28497  ballotlemsup  28640  ballotlem7  28671  subfacp1lem2a  28821  subfacp1lem2b  28822  erdszelem2  28833  kur14lem7  28853  kur14lem9  28855  dfon2lem2  29433  wfrlem14  29573  bpoly4  30026  opnmbllem0  30255  mblfinlem3  30258  mblfinlem4  30259  ismblfin  30260  volsupnfl  30264  sdclem2  30440  heibor1lem  30510  ismrc  30838  mapfzcons1cl  30855  2rexfrabdioph  30934  3rexfrabdioph  30935  4rexfrabdioph  30936  6rexfrabdioph  30937  7rexfrabdioph  30938  rabdiophlem2  30940  jm2.27dlem5  31159  algbase  31331  algaddg  31332  algmulr  31333  algsca  31334  algvsca  31335  lhe4.4ex1a  31438  dvcosre  31909  fourierdlem46  32138  fourierdlem57  32149  fourierdlem58  32150  fourierdlem62  32154  fourierdlem102  32194  fourierdlem103  32195  fourierdlem104  32196  fourierdlem114  32206  dmmpt2ssx2  33070  aacllem  33360  bnj931  33972  bnj1137  34194  bj-snglsstag  34682  bj-2upln1upl  34725  bj-ccssccbar  34763  bj-ccinftyssccbar  34764  dicval  37046  dvhdimlem  37314  intimass2  37929
  Copyright terms: Public domain W3C validator