Metamath Proof Explorer


Theorem fnimatp

Description: The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses fnimatp.1 φ F Fn D
fnimatp.2 φ A D
fnimatp.3 φ B D
fnimatp.4 φ C D
Assertion fnimatp φ F A B C = F A F B F C

Proof

Step Hyp Ref Expression
1 fnimatp.1 φ F Fn D
2 fnimatp.2 φ A D
3 fnimatp.3 φ B D
4 fnimatp.4 φ C D
5 fnimapr F Fn D A D B D F A B = F A F B
6 1 2 3 5 syl3anc φ F A B = F A F B
7 fnsnfv F Fn D C D F C = F C
8 1 4 7 syl2anc φ F C = F C
9 8 eqcomd φ F C = F C
10 6 9 uneq12d φ F A B F C = F A F B F C
11 df-tp A B C = A B C
12 11 imaeq2i F A B C = F A B C
13 imaundi F A B C = F A B F C
14 12 13 eqtri F A B C = F A B F C
15 df-tp F A F B F C = F A F B F C
16 10 14 15 3eqtr4g φ F A B C = F A F B F C