Theorem ressid 17183

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 3958	. 2 ⊢ 𝐵 ⊆ 𝐵
2		ressid.1	. . 3 ⊢ 𝐵 = (Base‘𝑊)
3	2	fvexi 6856	. 2 ⊢ 𝐵 ∈ V
4		eqid 2737	. . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵)
5	4, 2	ressid2 17173	. 2 ⊢ ((𝐵 ⊆ 𝐵 ∧ 𝑊 ∈ 𝑋 ∧ 𝐵 ∈ V) → (𝑊 ↾s 𝐵) = 𝑊)
6	1, 3, 5	mp3an13 1455	1 ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  ‘cfv 6500  (class class class)co 7368  Basecbs 17148   ↾_s cress 17169

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-ress 17170

This theorem is referenced by:  ressval3d  17185  submgmid  18643  submid  18747  subgid  19070  gaid2  19244  subrngid  20494  subrgid  20518  sdrgid  20737  rlmval2  21156  rlmsca  21162  rlmsca2  21163  pjff  21679  dsmmfi  21705  frlmip  21745  evlrhm  22068  evlsscasrng  22072  evlsvarsrng  22074  evl1sca  22290  evl1var  22292  evls1scasrng  22295  evls1varsrng  22296  pf1ind  22311  evl1gsumadd  22314  evl1varpw  22317  ressply1evl  22326  cnstrcvs  25109  cncvs  25113  rlmbn  25329  ishl2  25338  rrxprds  25357  dchrptlem2  27244  evl1fpws  33657  evlextv  33719  resssra  33764  rgmoddimOLD  33788  qusdimsum  33806  fldextid  33837  riccrng1  42891  ricdrng1  42898  evlsevl  42932  evlvvval  42933  evlvvvallem  42934  mhphf4  42958  lnmfg  43439  lmhmfgsplit  43443  pwslnmlem2  43450  simpcntrab  47228