Metamath Proof Explorer

Theorem bj-evalf

Description: The evaluation at a class is a function from the universal class into the universal class. (Contributed by BJ, 17-Mar-2026)

Ref Expression
Assertion bj-evalf 
|- Slot A : _V --> _V

Proof

Step Hyp Ref Expression
1 df-slot 
 |-  Slot A = ( f e. _V |-> ( f ` A ) )
2 fvexd 
 |-  ( f e. _V -> ( f ` A ) e. _V )
3 1 2 fmpti 
 |-  Slot A : _V --> _V