Theorem elab2g

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995)

	Ref	Expression
Hypotheses	elab2g.1	|- ( x = A -> ( ph <-> ps ) )
	elab2g.2	|- B = { x | ph }
Assertion	elab2g	|- ( A e. V -> ( A e. B <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		elab2g.1	|- ( x = A -> ( ph <-> ps ) )
2		elab2g.2	|- B = { x | ph }
3	2	eleq2i	|- ( A e. B <-> A e. { x | ph } )
4	1	elabg	|- ( A e. V -> ( A e. { x | ph } <-> ps ) )
5	3 4	bitrid	|- ( A e. V -> ( A e. B <-> ps ) )