Metamath Proof Explorer

Theorem pjmfn

Description: Functionality of the projection function. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjmfn proj Fn C


Step Hyp Ref Expression
1 ax-hilex V
2 1 mptex x ι z h | y h x = z + y V
3 df-pjh proj = h C x ι z h | y h x = z + y
4 2 3 fnmpti proj Fn C