Description: The value of a member of the domain of a subclass of a function. (Contributed by NM, 15-Aug-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | funssfv | ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvres | ⊢ ( 𝐴 ∈ dom 𝐺 → ( ( 𝐹 ↾ dom 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) | |
2 | 1 | eqcomd | ⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐹 ‘ 𝐴 ) = ( ( 𝐹 ↾ dom 𝐺 ) ‘ 𝐴 ) ) |
3 | funssres | ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 ) | |
4 | 3 | fveq1d | ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( ( 𝐹 ↾ dom 𝐺 ) ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) |
5 | 2 4 | sylan9eqr | ⊢ ( ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) |
6 | 5 | 3impa | ⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) |