Metamath Proof Explorer

Theorem fvreseq1

Description: Equality of a function restricted to the domain of another function. (Contributed by AV, 6-Jan-2019)

Ref Expression
Assertion fvreseq1 ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A → F ↾ B = G ↔ ∀ x ∈ B F ⁡ x = G ⁡ x

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ G Fn B → G ↾ B = G
2 1 ad2antlr ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A → G ↾ B = G
3 2 eqcomd ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A → G = G ↾ B
4 3 eqeq2d ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A → F ↾ B = G ↔ F ↾ B = G ↾ B
5 ssid ⊢ B ⊆ B
6 fvreseq0 ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A ∧ B ⊆ B → F ↾ B = G ↾ B ↔ ∀ x ∈ B F ⁡ x = G ⁡ x
7 5 6 mpanr2 ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A → F ↾ B = G ↾ B ↔ ∀ x ∈ B F ⁡ x = G ⁡ x
8 4 7 bitrd ⊢ F Fn A ∧ G Fn B ∧ B ⊆ A → F ↾ B = G ↔ ∀ x ∈ B F ⁡ x = G ⁡ x