Theorem clabel

Description: Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006)

	Ref	Expression
Assertion	clabel	|- ( { x | ph } e. A <-> E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( { x | ph } e. A <-> E. y ( y = { x | ph } /\ y e. A ) )
2		abeq2	|- ( y = { x | ph } <-> A. x ( x e. y <-> ph ) )
3	2	anbi2ci	|- ( ( y = { x | ph } /\ y e. A ) <-> ( y e. A /\ A. x ( x e. y <-> ph ) ) )
4	3	exbii	|- ( E. y ( y = { x | ph } /\ y e. A ) <-> E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) )
5	1 4	bitri	|- ( { x | ph } e. A <-> E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) )