Theorem ressid 17290

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  ‘cfv 6561  (class class class)co 7431  Basecbs 17247   ↾_s cress 17274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-ress 17275

This theorem is referenced by:  ressval3d  17292  submgmid  18719  submid  18823  subgid  19146  gaid2  19321  subrngid  20549  subrgid  20573  sdrgid  20793  rlmval2  21199  rlmsca  21205  rlmsca2  21206  pjff  21732  dsmmfi  21758  frlmip  21798  evlrhm  22120  evlsscasrng  22121  evlsvarsrng  22123  evl1sca  22338  evl1var  22340  evls1scasrng  22343  evls1varsrng  22344  pf1ind  22359  evl1gsumadd  22362  evl1varpw  22365  ressply1evl  22374  cnstrcvs  25174  cncvs  25178  rlmbn  25395  ishl2  25404  rrxprds  25423  dchrptlem2  27309  evl1fpws  33590  resssra  33638  rgmoddimOLD  33661  qusdimsum  33679  fldextid  33710  riccrng1  42531  ricdrng1  42538  evlsevl  42581  evlvvval  42583  evlvvvallem  42584  mhphf4  42610  lnmfg  43094  lmhmfgsplit  43098  pwslnmlem2  43105  simpcntrab  46885