Metamath Proof Explorer


Theorem chpcl

Description: Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion chpcl A ψ A

Proof

Step Hyp Ref Expression
1 chpf ψ :
2 1 ffvelrni A ψ A