Theorem rexab2

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	|- ( x = y -> ( ps <-> ch ) )
2		df-rex	|- ( E. x e. { y | ph } ps <-> E. x ( x e. { y | ph } /\ ps ) )
3		nfsab1	|- F/ y x e. { y | ph }
4		nfv	|- F/ y ps
5	3 4	nfan	|- F/ y ( x e. { y | ph } /\ ps )
6		nfv	|- F/ x ( ph /\ ch )
7		eleq1ab	|- ( x = y -> ( x e. { y | ph } <-> y e. { y | ph } ) )
8		abid	|- ( y e. { y | ph } <-> ph )
9	7 8	bitrdi	|- ( x = y -> ( x e. { y | ph } <-> ph ) )
10	9 1	anbi12d	|- ( x = y -> ( ( x e. { y | ph } /\ ps ) <-> ( ph /\ ch ) ) )
11	5 6 10	cbvexv1	|- ( E. x ( x e. { y | ph } /\ ps ) <-> E. y ( ph /\ ch ) )
12	2 11	bitri	|- ( E. x e. { y | ph } ps <-> E. y ( ph /\ ch ) )