Theorem ressid 17205

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 3937	. 2 ⊢ 𝐵 ⊆ 𝐵
2		ressid.1	. . 3 ⊢ 𝐵 = (Base‘𝑊)
3	2	fvexi 6841	. 2 ⊢ 𝐵 ∈ V
4		eqid 2739	. . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵)
5	4, 2	ressid2 17195	. 2 ⊢ ((𝐵 ⊆ 𝐵 ∧ 𝑊 ∈ 𝑋 ∧ 𝐵 ∈ V) → (𝑊 ↾s 𝐵) = 𝑊)
6	1, 3, 5	mp3an13 1460	1 ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ⊆ wss 3883  ‘cfv 6485  (class class class)co 7356  Basecbs 17170   ↾_s cress 17191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-ress 17192

This theorem is referenced by:  ressval3d  17207  submgmid  18665  submid  18769  subgid  19095  gaid2  19269  subrngid  20521  subrgid  20545  sdrgid  20764  rlmval2  21182  rlmsca  21188  rlmsca2  21189  pjff  21687  dsmmfi  21713  frlmip  21753  evlrhm  22077  evlsscasrng  22081  evlsvarsrng  22083  evlsevl  22108  evlvvval  22109  evl1sca  22320  evl1var  22322  evls1scasrng  22325  evls1varsrng  22326  pf1ind  22341  evl1gsumadd  22344  evl1varpw  22347  ressply1evl  22356  cnstrcvs  25126  cncvs  25130  rlmbn  25346  ishl2  25355  rrxprds  25374  dchrptlem2  27246  evl1fpws  33647  evlextv  33726  resssra  33771  qusdimsum  33812  fldextid  33843  riccrng1  43007  ricdrng1  43014  evlvvvallem  43037  mhphf4  43050  lnmfg  43527  lmhmfgsplit  43531  pwslnmlem2  43538  simpcntrab  47313