This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )