Theorem bj-abex

Description: Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-abex	|- ( { x | ph } e. _V <-> E. y A. x ( x e. y <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		isset	|- ( { x | ph } e. _V <-> E. y y = { x | ph } )
2		eqabb	|- ( y = { x | ph } <-> A. x ( x e. y <-> ph ) )
3	2	exbii	|- ( E. y y = { x | ph } <-> E. y A. x ( x e. y <-> ph ) )
4	1 3	bitri	|- ( { x | ph } e. _V <-> E. y A. x ( x e. y <-> ph ) )