Theorem fvres

Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	fvres	⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	brresi	⊢ ( 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 𝐹 𝑥 ) )
3	2	baib	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ↔ 𝐴 𝐹 𝑥 ) )
4	3	iotabidv	⊢ ( 𝐴 ∈ 𝐵 → ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) )
5		df-fv	⊢ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( ℩ 𝑥 𝐴 ( 𝐹 ↾ 𝐵 ) 𝑥 )
6		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 )
7	4 5 6	3eqtr4g	⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )