Theorem clelab

Description: Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993) (Proof shortened by Wolf Lammen, 16-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( A e. { x | ph } <-> E. y ( y = A /\ y e. { x | ph } ) )
2		nfv	|- F/ y ( x = A /\ ph )
3		nfv	|- F/ x y = A
4		nfsab1	|- F/ x y e. { x | ph }
5	3 4	nfan	|- F/ x ( y = A /\ y e. { x | ph } )
6		eqeq1	|- ( x = y -> ( x = A <-> y = A ) )
7		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
8		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
9	7 8	syl6bbr	|- ( x = y -> ( ph <-> y e. { x | ph } ) )
10	6 9	anbi12d	|- ( x = y -> ( ( x = A /\ ph ) <-> ( y = A /\ y e. { x | ph } ) ) )
11	2 5 10	cbvexv1	|- ( E. x ( x = A /\ ph ) <-> E. y ( y = A /\ y e. { x | ph } ) )
12	1 11	bitr4i	|- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) )