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

Metamath Proof Explorer

Theorem elrab

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999) Remove dependency on ax-13 . (Revised by Steven Nguyen, 23-Nov-2022)

Ref Expression
Hypothesis elrab.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion elrab 
|- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )

Proof

Step Hyp Ref Expression
1 elrab.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 elex 
 |-  ( A e. { x e. B | ph } -> A e. _V )
3 elex 
 |-  ( A e. B -> A e. _V )
4 3 adantr 
 |-  ( ( A e. B /\ ps ) -> A e. _V )
5 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
6 5 1 anbi12d 
 |-  ( x = A -> ( ( x e. B /\ ph ) <-> ( A e. B /\ ps ) ) )
7 df-rab 
 |-  { x e. B | ph } = { x | ( x e. B /\ ph ) }
8 6 7 elab2g 
 |-  ( A e. _V -> ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) ) )
9 2 4 8 pm5.21nii 
 |-  ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )