MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseqtrri Structured version   Visualization version   GIF version

Theorem sseqtrri 4002
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtrri.1 𝐴𝐵
sseqtrri.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtrri 𝐴𝐶

Proof of Theorem sseqtrri
StepHypRef Expression
1 sseqtrri.1 . 2 𝐴𝐵
2 sseqtrri.2 . . 3 𝐶 = 𝐵
32eqcomi 2828 . 2 𝐵 = 𝐶
41, 3sseqtri 4001 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wss 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950
This theorem is referenced by:  eqimss2i  4024  difsssymdif  4227  snsspr1  4739  snsspr2  4740  snsstp1  4741  snsstp2  4742  snsstp3  4743  unissint  4891  iunxdif2  4968  pwpwssunieq  5017  intabs  5236  inxpssres  5565  opabssxp  5636  dmresi  5914  cnvimass  5942  sofld  6037  cnvcnv  6042  cnvssrndm  6115  sssucid  6261  fvclss  6993  dmmpossx  7756  suppun  7842  wfrlem14  7960  tfrlem11  8016  oawordeulem  8172  mapex  8404  trcl  9162  djuunxp  9342  dfac3  9539  cfsuc  9671  isfin4p1  9729  fin23lem11  9731  domtriomlem  9856  ttukeylem1  9923  ttukeylem7  9929  brdom7disj  9945  brdom6disj  9946  fingch  10037  fpwwe2lem13  10056  canthp1lem2  10067  wunex2  10152  wunex3  10155  ressxr  10677  ltrelxr  10694  nnssnn0  11892  un0addcl  11922  un0mulcl  11923  nn0ssxnn0  11962  caubnd  14710  isumclim3  15106  iprodclim3  15346  bpoly4  15405  fprodefsum  15440  znnen  15557  isprm3  16019  phimullem  16108  isstruct2  16485  2strbas  16595  2strop  16596  2strbas1  16598  rngbase  16612  rngplusg  16613  rngmulr  16614  srngbase  16620  srngplusg  16621  srngmulr  16622  srnginvl  16623  lmodbase  16629  lmodplusg  16630  lmodsca  16631  lmodvsca  16632  ipsbase  16636  ipsaddg  16637  ipsmulr  16638  ipssca  16639  ipsvsca  16640  ipsip  16641  phlbase  16646  phlplusg  16647  phlsca  16648  phlvsca  16649  phlip  16650  topgrpbas  16654  topgrpplusg  16655  topgrptset  16656  otpsbas  16661  otpstset  16662  otpsle  16663  odrngbas  16672  odrngplusg  16673  odrngmulr  16674  odrngtset  16675  odrngle  16676  odrngds  16677  homarw  17298  ipoval  17756  ipolerval  17758  eqgfval  18320  cycsubg  18343  symgbas  18491  symgsubmefmndALT  18523  islbs3  19919  cnfldbas  20541  cnfldadd  20542  cnfldmul  20543  cnfldcj  20544  cnfldtset  20545  cnfldle  20546  cnfldds  20547  cnfldunif  20548  basdif0  21553  iscldtop  21695  iocpnfordt  21815  icomnfordt  21816  iooordt  21817  cnrest2  21886  cmpcov2  21990  fiuncmp  22004  bwth  22010  indisconn  22018  locfincmp  22126  xkococnlem  22259  hmphdis  22396  uzrest  22497  ufildr  22531  fin1aufil  22532  eltsms  22733  ustval  22803  qtopbaslem  23359  tgqioo  23400  re2ndc  23401  xrhmeo  23542  bndth  23554  pi1xfrcnvlem  23652  ovolficcss  24062  nulmbl2  24129  uniiccdif  24171  opnmbllem  24194  opnmblALT  24196  mbfimaopnlem  24248  i1fima  24271  i1fima2  24272  i1fd  24274  c1liplem1  24585  deg1n0ima  24675  efcvx  25029  dvrelog  25212  dvloglem  25223  logf1o2  25225  dvlog  25226  ressatans  25504  wilthlem3  25639  trkgbas  26223  trkgdist  26224  trkgitv  26225  ex-ss  28198  ajfval  28578  ipasslem8  28606  hlimcaui  29005  shsspwh  29015  hhssabloi  29031  hhssnv  29033  hhshsslem1  29036  shunssji  29138  sshhococi  29315  pjoml6i  29358  osumcori  29412  mayete3i  29497  mayetes3i  29498  imaelshi  29827  pjclem1  29964  pjci  29969  mdcompli  30198  dmdcompli  30199  xppreima  30386  gsummpt2co  30679  cycpmrn  30778  circtopn  31094  esumpcvgval  31330  esumcvg  31338  ldgenpisyslem3  31417  elmbfmvol2  31518  sxbrsigalem0  31522  eulerpartlemsv3  31612  ballotlem7  31786  rpsqrtcn  31857  bnj931  32035  bnj1137  32260  subfacp1lem2a  32420  subfacp1lem2b  32421  erdszelem2  32432  kur14lem7  32452  kur14lem9  32454  dfon2lem2  33022  frrlem12  33127  bj-snglsstag  34286  bj-2upln1upl  34329  bj-0int  34385  bj-opabssvv  34434  bj-ccssccbar  34491  bj-ccinftyssccbar  34492  bj-rvecsscvec  34577  icoreelrn  34634  finxpreclem3  34666  imadifss  34859  poimirlem4  34888  poimirlem26  34910  poimirlem27  34911  opnmbllem0  34920  mblfinlem3  34923  mblfinlem4  34924  ismblfin  34925  volsupnfl  34929  sdclem2  35009  heibor1lem  35079  refrelsredund4  35859  dicval  38304  dvhdimlem  38572  ismrc  39288  mapfzcons1cl  39305  2rexfrabdioph  39383  3rexfrabdioph  39384  4rexfrabdioph  39385  6rexfrabdioph  39386  7rexfrabdioph  39387  rabdiophlem2  39389  jm2.27dlem5  39600  algbase  39768  algaddg  39769  algmulr  39770  algsca  39771  algvsca  39772  intimass2  39990  comptiunov2i  40041  relexp0a  40051  lhe4.4ex1a  40651  iocnct  41805  iccnct  41806  dvcosre  42185  fourierdlem46  42427  fourierdlem57  42438  fourierdlem58  42439  fourierdlem62  42443  fourierdlem102  42483  fourierdlem103  42484  fourierdlem104  42485  fourierdlem114  42495  sge0split  42681  sge0uzfsumgt  42716  hoiprodp1  42860  hoidmvlelem1  42867  hoidmvlelem2  42868  hoidmvlelem3  42869  sbgoldbo  43942  dmmpossx2  44375  aacllem  44892
  Copyright terms: Public domain W3C validator