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

Metamath Proof Explorer

Theorem fvreseq0

Description: Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 fnssres ⊢ F Fn A ∧ B ⊆ A → F ↾ B Fn B
2 fnssres ⊢ G Fn C ∧ B ⊆ C → G ↾ B Fn B
3 eqfnfv ⊢ F ↾ B Fn B ∧ G ↾ B Fn B → F ↾ B = G ↾ B ↔ ∀ x ∈ B F ↾ B ⁡ x = G ↾ B ⁡ x
4 fvres ⊢ x ∈ B → F ↾ B ⁡ x = F ⁡ x
5 fvres ⊢ x ∈ B → G ↾ B ⁡ x = G ⁡ x
6 4 5 eqeq12d ⊢ x ∈ B → F ↾ B ⁡ x = G ↾ B ⁡ x ↔ F ⁡ x = G ⁡ x
7 6 ralbiia ⊢ ∀ x ∈ B F ↾ B ⁡ x = G ↾ B ⁡ x ↔ ∀ x ∈ B F ⁡ x = G ⁡ x
8 3 7 bitrdi ⊢ F ↾ B Fn B ∧ G ↾ B Fn B → F ↾ B = G ↾ B ↔ ∀ x ∈ B F ⁡ x = G ⁡ x
9 1 2 8 syl2an ⊢ F Fn A ∧ B ⊆ A ∧ G Fn C ∧ B ⊆ C → F ↾ B = G ↾ B ↔ ∀ x ∈ B F ⁡ x = G ⁡ x
10 9 an4s ⊢ F Fn A ∧ G Fn C ∧ B ⊆ A ∧ B ⊆ C → F ↾ B = G ↾ B ↔ ∀ x ∈ B F ⁡ x = G ⁡ x