Theorem ralrab2

Description: Universal quantification over a restricted class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	|- ( x = y -> ( ps <-> ch ) )
2		df-rab	|- { y e. A | ph } = { y | ( y e. A /\ ph ) }
3	2	raleqi	|- ( A. x e. { y e. A | ph } ps <-> A. x e. { y | ( y e. A /\ ph ) } ps )
4	1	ralab2	|- ( A. x e. { y | ( y e. A /\ ph ) } ps <-> A. y ( ( y e. A /\ ph ) -> ch ) )
5		impexp	|- ( ( ( y e. A /\ ph ) -> ch ) <-> ( y e. A -> ( ph -> ch ) ) )
6	5	albii	|- ( A. y ( ( y e. A /\ ph ) -> ch ) <-> A. y ( y e. A -> ( ph -> ch ) ) )
7		df-ral	|- ( A. y e. A ( ph -> ch ) <-> A. y ( y e. A -> ( ph -> ch ) ) )
8	6 7	bitr4i	|- ( A. y ( ( y e. A /\ ph ) -> ch ) <-> A. y e. A ( ph -> ch ) )
9	3 4 8	3bitri	|- ( A. x e. { y e. A | ph } ps <-> A. y e. A ( ph -> ch ) )