Theorem elrab2

Description: Membership in a restricted 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 ) )