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 ffvelcdmi AψA