Theorem rexrab

Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Mario Carneiro, 3-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ralab.1	|- ( y = x -> ( ph <-> ps ) )
2	1	elrab	|- ( x e. { y e. A | ph } <-> ( x e. A /\ ps ) )
3	2	anbi1i	|- ( ( x e. { y e. A | ph } /\ ch ) <-> ( ( x e. A /\ ps ) /\ ch ) )
4		anass	|- ( ( ( x e. A /\ ps ) /\ ch ) <-> ( x e. A /\ ( ps /\ ch ) ) )
5	3 4	bitri	|- ( ( x e. { y e. A | ph } /\ ch ) <-> ( x e. A /\ ( ps /\ ch ) ) )
6	5	rexbii2	|- ( E. x e. { y e. A | ph } ch <-> E. x e. A ( ps /\ ch ) )