Metamath Proof Explorer

Theorem fnimapr

Description: The image of a pair under a function. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Assertion fnimapr ⊢ F Fn A ∧ B ∈ A ∧ C ∈ A → F B C = F ⁡ B F ⁡ C

Proof

Step Hyp Ref Expression
1 fnsnfv ⊢ F Fn A ∧ B ∈ A → F ⁡ B = F B
2 1 3adant3 ⊢ F Fn A ∧ B ∈ A ∧ C ∈ A → F ⁡ B = F B
3 fnsnfv ⊢ F Fn A ∧ C ∈ A → F ⁡ C = F C
4 3 3adant2 ⊢ F Fn A ∧ B ∈ A ∧ C ∈ A → F ⁡ C = F C
5 2 4 uneq12d ⊢ F Fn A ∧ B ∈ A ∧ C ∈ A → F ⁡ B ∪ F ⁡ C = F B ∪ F C
6 5 eqcomd ⊢ F Fn A ∧ B ∈ A ∧ C ∈ A → F B ∪ F C = F ⁡ B ∪ F ⁡ C
7 df-pr ⊢ B C = B ∪ C
8 7 imaeq2i ⊢ F B C = F B ∪ C
9 imaundi ⊢ F B ∪ C = F B ∪ F C
10 8 9 eqtri ⊢ F B C = F B ∪ F C
11 df-pr ⊢ F ⁡ B F ⁡ C = F ⁡ B ∪ F ⁡ C
12 6 10 11 3eqtr4g ⊢ F Fn A ∧ B ∈ A ∧ C ∈ A → F B C = F ⁡ B F ⁡ C