Metamath Proof Explorer


Theorem pjfn

Description: Functionality of a projection. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion pjfn HCprojHFn

Proof

Step Hyp Ref Expression
1 pjhf HCprojH:
2 1 ffnd HCprojHFn