Theorem elab3g

Description: Membership in a class abstraction, with a weaker antecedent than elabg . (Contributed by NM, 29-Aug-2006)

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

Proof

Step	Hyp	Ref	Expression
1		elab3g.1	|- ( x = A -> ( ph <-> ps ) )
2	1	elabg	|- ( A e. { x | ph } -> ( A e. { x | ph } <-> ps ) )
3	2	ibi	|- ( A e. { x | ph } -> ps )
4		pm2.21	|- ( -. ps -> ( ps -> A e. { x | ph } ) )
5	3 4	impbid2	|- ( -. ps -> ( A e. { x | ph } <-> ps ) )
6	1	elabg	|- ( A e. B -> ( A e. { x | ph } <-> ps ) )
7	5 6	ja	|- ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) )