Metamath Proof Explorer


Theorem elrab2

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006)

Ref Expression
Hypotheses elrab2.1
|- ( x = A -> ( ph <-> ps ) )
elrab2.2
|- C = { x e. B | ph }
Assertion elrab2
|- ( A e. C <-> ( A e. B /\ ps ) )

Proof

Step Hyp Ref Expression
1 elrab2.1
 |-  ( x = A -> ( ph <-> ps ) )
2 elrab2.2
 |-  C = { x e. B | ph }
3 2 eleq2i
 |-  ( A e. C <-> A e. { x e. B | ph } )
4 1 elrab
 |-  ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
5 3 4 bitri
 |-  ( A e. C <-> ( A e. B /\ ps ) )