Theorem bj-clex

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

	Ref	Expression
Hypothesis	bj-clex.1	|- ( x e. A <-> ph )
Assertion	bj-clex	|- ( A e. _V <-> E. y A. x ( x e. y <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		bj-clex.1	|- ( x e. A <-> ph )
2		isset	|- ( A e. _V <-> E. y y = A )
3		dfcleq	|- ( y = A <-> A. x ( x e. y <-> x e. A ) )
4	1	bibi2i	|- ( ( x e. y <-> x e. A ) <-> ( x e. y <-> ph ) )
5	4	albii	|- ( A. x ( x e. y <-> x e. A ) <-> A. x ( x e. y <-> ph ) )
6	3 5	bitri	|- ( y = A <-> A. x ( x e. y <-> ph ) )
7	6	exbii	|- ( E. y y = A <-> E. y A. x ( x e. y <-> ph ) )
8	2 7	bitri	|- ( A e. _V <-> E. y A. x ( x e. y <-> ph ) )