Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Relations and Functions
Functions - misc additions
fnimatp
Next ⟩
fnunres2
Metamath Proof Explorer
Ascii
Unicode
Theorem
fnimatp
Description:
The image of a triplet 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