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

Theorem ressid 17173
Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
Hypothesis
Ref Expression
ressid.1 𝐵 = (Base‘𝑊)
Assertion
Ref Expression
ressid (𝑊𝑋 → (𝑊s 𝐵) = 𝑊)

Proof of Theorem ressid
StepHypRef Expression
1 ssid 4001 . 2 𝐵𝐵
2 ressid.1 . . 3 𝐵 = (Base‘𝑊)
32fvexi 6893 . 2 𝐵 ∈ V
4 eqid 2732 . . 3 (𝑊s 𝐵) = (𝑊s 𝐵)
54, 2ressid2 17161 . 2 ((𝐵𝐵𝑊𝑋𝐵 ∈ V) → (𝑊s 𝐵) = 𝑊)
61, 3, 5mp3an13 1452 1 (𝑊𝑋 → (𝑊s 𝐵) = 𝑊)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  Vcvv 3474  wss 3945  cfv 6533  (class class class)co 7394  Basecbs 17128  s cress 17157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pr 5421
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3775  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7397  df-oprab 7398  df-mpo 7399  df-ress 17158
This theorem is referenced by:  ressval3d  17175  ressval3dOLD  17176  submid  18669  subgid  18982  gaid2  19135  subrgid  20316  sdrgid  20359  rlmval2  20766  rlmsca  20772  rlmsca2  20773  pjff  21202  dsmmfi  21228  frlmip  21268  evlrhm  21590  evlsscasrng  21591  evlsvarsrng  21593  evl1sca  21784  evl1var  21786  evls1scasrng  21789  evls1varsrng  21790  pf1ind  21805  evl1gsumadd  21808  evl1varpw  21811  cnstrcvs  24588  cncvs  24592  rlmbn  24809  ishl2  24818  rrxprds  24837  dchrptlem2  26697  ressply1evl  32554  rgmoddim  32597  qusdimsum  32615  fldextid  32640  riccrng1  40964  ricdrng1  40970  evlsevl  41002  mhphf4  41024  lnmfg  41659  lmhmfgsplit  41663  pwslnmlem2  41670  simpcntrab  45423  submgmid  46399
  Copyright terms: Public domain W3C validator