Theorem abexex

Description: A condition where a class abstraction continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007)

	Ref	Expression
Hypotheses	abexex.1	|- A e. _V
	abexex.2	|- ( ph -> x e. A )
	abexex.3	|- { y | ph } e. _V
Assertion	abexex	|- { y | E. x ph } e. _V

Proof

Step	Hyp	Ref	Expression
1		abexex.1	|- A e. _V
2		abexex.2	|- ( ph -> x e. A )
3		abexex.3	|- { y | ph } e. _V
4		df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
5	2	pm4.71ri	|- ( ph <-> ( x e. A /\ ph ) )
6	5	exbii	|- ( E. x ph <-> E. x ( x e. A /\ ph ) )
7	4 6	bitr4i	|- ( E. x e. A ph <-> E. x ph )
8	7	abbii	|- { y | E. x e. A ph } = { y | E. x ph }
9	1 3	abrexex2	|- { y | E. x e. A ph } e. _V
10	8 9	eqeltrri	|- { y | E. x ph } e. _V