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

Step	Hyp	Ref	Expression
1		ssid 4001	. 2 ⊢ 𝐵 ⊆ 𝐵
2		ressid.1	. . 3 ⊢ 𝐵 = (Base‘𝑊)
3	2	fvexi 6893	. 2 ⊢ 𝐵 ∈ V
4		eqid 2732	. . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵)
5	4, 2	ressid2 17161	. 2 ⊢ ((𝐵 ⊆ 𝐵 ∧ 𝑊 ∈ 𝑋 ∧ 𝐵 ∈ V) → (𝑊 ↾s 𝐵) = 𝑊)
6	1, 3, 5	mp3an13 1452	1 ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)

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