Theorem elab4g

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		elab4g.1	|- ( x = A -> ( ph <-> ps ) )
2		elab4g.2	|- B = { x | ph }
3		elex	|- ( A e. B -> A e. _V )
4	1 2	elab2g	|- ( A e. _V -> ( A e. B <-> ps ) )
5	3 4	biadanii	|- ( A e. B <-> ( A e. _V /\ ps ) )