This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvres

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

Ref Expression
Assertion fvres ⊢ A ∈ B → F ↾ B ⁡ A = F ⁡ A

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 brresi ⊢ A F ↾ B x ↔ A ∈ B ∧ A F x
3 2 baib ⊢ A ∈ B → A F ↾ B x ↔ A F x
4 3 iotabidv ⊢ A ∈ B → ι x | A F ↾ B x = ι x | A F x
5 df-fv ⊢ F ↾ B ⁡ A = ι x | A F ↾ B x
6 df-fv ⊢ F ⁡ A = ι x | A F x
7 4 5 6 3eqtr4g ⊢ A ∈ B → F ↾ B ⁡ A = F ⁡ A