Theorem ressid 16982

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 3945	. 2 ⊢ 𝐵 ⊆ 𝐵
2		ressid.1	. . 3 ⊢ 𝐵 = (Base‘𝑊)
3	2	fvexi 6806	. 2 ⊢ 𝐵 ∈ V
4		eqid 2733	. . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵)
5	4, 2	ressid2 16973	. 2 ⊢ ((𝐵 ⊆ 𝐵 ∧ 𝑊 ∈ 𝑋 ∧ 𝐵 ∈ V) → (𝑊 ↾s 𝐵) = 𝑊)
6	1, 3, 5	mp3an13 1450	1 ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2101  Vcvv 3434   ⊆ wss 3889  ‘cfv 6447  (class class class)co 7295  Basecbs 16940   ↾_s cress 16969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3224  df-v 3436  df-sbc 3719  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-br 5078  df-opab 5140  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-iota 6399  df-fun 6449  df-fv 6455  df-ov 7298  df-oprab 7299  df-mpo 7300  df-ress 16970

This theorem is referenced by:  ressval3d  16984  ressval3dOLD  16985  submid  18477  subgid  18785  gaid2  18937  subrgid  20054  sdrgid  20092  rlmval2  20492  rlmsca  20498  rlmsca2  20499  pjff  20947  dsmmfi  20973  frlmip  21013  evlrhm  21334  evlsscasrng  21335  evlsvarsrng  21337  evl1sca  21528  evl1var  21530  evls1scasrng  21533  evls1varsrng  21534  pf1ind  21549  evl1gsumadd  21552  evl1varpw  21555  cnstrcvs  24332  cncvs  24336  rlmbn  24553  ishl2  24562  rrxprds  24581  dchrptlem2  26441  rgmoddim  31721  qusdimsum  31737  fldextid  31762  mhphf4  40311  lnmfg  40931  lmhmfgsplit  40935  pwslnmlem2  40942  simpcntrab  44426  submgmid  45387