Theorem elrabi

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017)

	Ref	Expression
Assertion	elrabi	|- ( A e. { x e. V | ph } -> A e. V )

Proof

Step	Hyp	Ref	Expression
1		clelab	|- ( A e. { x | ( x e. V /\ ph ) } <-> E. x ( x = A /\ ( x e. V /\ ph ) ) )
2		eleq1	|- ( x = A -> ( x e. V <-> A e. V ) )
3	2	anbi1d	|- ( x = A -> ( ( x e. V /\ ph ) <-> ( A e. V /\ ph ) ) )
4	3	simprbda	|- ( ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
5	4	exlimiv	|- ( E. x ( x = A /\ ( x e. V /\ ph ) ) -> A e. V )
6	1 5	sylbi	|- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
7		df-rab	|- { x e. V | ph } = { x | ( x e. V /\ ph ) }
8	6 7	eleq2s	|- ( A e. { x e. V | ph } -> A e. V )