Theorem ressid

Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

	Ref	Expression
Hypothesis	ressid.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	ressid	⊢ ( 𝑊 ∈ 𝑋 → ( 𝑊 ↾s 𝐵 ) = 𝑊 )

Proof

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