Metamath Proof Explorer


Theorem 1arympt1fv

Description: The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024)

Ref Expression
Hypothesis 1arympt1.f F=xX0Ax0
Assertion 1arympt1fv XVBXF0B=AB

Proof

Step Hyp Ref Expression
1 1arympt1.f F=xX0Ax0
2 1 a1i XVBXF=xX0Ax0
3 fveq1 x=0Bx0=0B0
4 3 adantl XVBXx=0Bx0=0B0
5 c0ex 0V
6 5 a1i XV0V
7 6 anim1i XVBX0VBX
8 7 adantr XVBXx=0B0VBX
9 fvsng 0VBX0B0=B
10 8 9 syl XVBXx=0B0B0=B
11 4 10 eqtrd XVBXx=0Bx0=B
12 11 fveq2d XVBXx=0BAx0=AB
13 5 a1i XVBX0V
14 simpr XVBXBX
15 13 14 fsnd XVBX0B:0X
16 snex 0V
17 16 a1i BX0V
18 elmapg XV0V0BX00B:0X
19 17 18 sylan2 XVBX0BX00B:0X
20 15 19 mpbird XVBX0BX0
21 fvexd XVBXABV
22 2 12 20 21 fvmptd XVBXF0B=AB