Theorem ralab

Description: Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024)

	Ref	Expression
Hypothesis	ralab.1	|- ( y = x -> ( ph <-> ps ) )
Assertion	ralab	|- ( A. x e. { y | ph } ch <-> A. x ( ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralab.1	|- ( y = x -> ( ph <-> ps ) )
2		df-ral	|- ( A. x e. { y | ph } ch <-> A. x ( x e. { y | ph } -> ch ) )
3		df-clab	|- ( x e. { y | ph } <-> [ x / y ] ph )
4	1	sbievw	|- ( [ x / y ] ph <-> ps )
5	3 4	bitri	|- ( x e. { y | ph } <-> ps )
6	5	imbi1i	|- ( ( x e. { y | ph } -> ch ) <-> ( ps -> ch ) )
7		biid	|- ( ( ps -> ch ) <-> ( ps -> ch ) )
8	6 7	bitri	|- ( ( x e. { y | ph } -> ch ) <-> ( ps -> ch ) )
9	8	albii	|- ( A. x ( x e. { y | ph } -> ch ) <-> A. x ( ps -> ch ) )
10	2 9	bitri	|- ( A. x e. { y | ph } ch <-> A. x ( ps -> ch ) )