Metamath Proof Explorer

Theorem oprssov

Description: The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007)

Ref Expression
Assertion oprssov ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F ∧ A ∈ C ∧ B ∈ D → A F B = A G B

Proof

Step Hyp Ref Expression
1 ovres ⊢ A ∈ C ∧ B ∈ D → A F ↾ C × D B = A F B
2 1 adantl ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F ∧ A ∈ C ∧ B ∈ D → A F ↾ C × D B = A F B
3 fndm ⊢ G Fn C × D → dom ⁡ G = C × D
4 3 reseq2d ⊢ G Fn C × D → F ↾ dom ⁡ G = F ↾ C × D
5 4 3ad2ant2 ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F → F ↾ dom ⁡ G = F ↾ C × D
6 funssres ⊢ Fun ⁡ F ∧ G ⊆ F → F ↾ dom ⁡ G = G
7 6 3adant2 ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F → F ↾ dom ⁡ G = G
8 5 7 eqtr3d ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F → F ↾ C × D = G
9 8 oveqd ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F → A F ↾ C × D B = A G B
10 9 adantr ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F ∧ A ∈ C ∧ B ∈ D → A F ↾ C × D B = A G B
11 2 10 eqtr3d ⊢ Fun ⁡ F ∧ G Fn C × D ∧ G ⊆ F ∧ A ∈ C ∧ B ∈ D → A F B = A G B