Theorem rexrab2

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

	Ref	Expression
Hypothesis	ralab2.1	|- ( x = y -> ( ps <-> ch ) )
Assertion	rexrab2	|- ( E. x e. { y e. A | ph } ps <-> E. 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	rexeqi	|- ( E. x e. { y e. A | ph } ps <-> E. x e. { y | ( y e. A /\ ph ) } ps )
4	1	rexab2	|- ( E. x e. { y | ( y e. A /\ ph ) } ps <-> E. y ( ( y e. A /\ ph ) /\ ch ) )
5		anass	|- ( ( ( y e. A /\ ph ) /\ ch ) <-> ( y e. A /\ ( ph /\ ch ) ) )
6	5	exbii	|- ( E. y ( ( y e. A /\ ph ) /\ ch ) <-> E. y ( y e. A /\ ( ph /\ ch ) ) )
7		df-rex	|- ( E. y e. A ( ph /\ ch ) <-> E. y ( y e. A /\ ( ph /\ ch ) ) )
8	6 7	bitr4i	|- ( E. y ( ( y e. A /\ ph ) /\ ch ) <-> E. y e. A ( ph /\ ch ) )
9	3 4 8	3bitri	|- ( E. x e. { y e. A | ph } ps <-> E. y e. A ( ph /\ ch ) )