Theorem elrabi

Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017) Remove disjoint variable condition on A , x and avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 5-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( A e. { x | ( x e. V /\ ph ) } <-> E. y ( y = A /\ y e. { x | ( x e. V /\ ph ) } ) )
2		df-clab	|- ( y e. { x | ( x e. V /\ ph ) } <-> [ y / x ] ( x e. V /\ ph ) )
3		simpl	|- ( ( x e. V /\ ph ) -> x e. V )
4	3	sbimi	|- ( [ y / x ] ( x e. V /\ ph ) -> [ y / x ] x e. V )
5		clelsb1	|- ( [ y / x ] x e. V <-> y e. V )
6	4 5	sylib	|- ( [ y / x ] ( x e. V /\ ph ) -> y e. V )
7	2 6	sylbi	|- ( y e. { x | ( x e. V /\ ph ) } -> y e. V )
8		eleq1	|- ( y = A -> ( y e. V <-> A e. V ) )
9	8	biimpa	|- ( ( y = A /\ y e. V ) -> A e. V )
10	7 9	sylan2	|- ( ( y = A /\ y e. { x | ( x e. V /\ ph ) } ) -> A e. V )
11	10	exlimiv	|- ( E. y ( y = A /\ y e. { x | ( x e. V /\ ph ) } ) -> A e. V )
12	1 11	sylbi	|- ( A e. { x | ( x e. V /\ ph ) } -> A e. V )
13		df-rab	|- { x e. V | ph } = { x | ( x e. V /\ ph ) }
14	12 13	eleq2s	|- ( A e. { x e. V | ph } -> A e. V )