Theorem elab3gf

Description: Membership in a class abstraction, with a weaker antecedent than elabgf . (Contributed by NM, 6-Sep-2011)

	Ref	Expression
Hypotheses	elab3gf.1	|- F/_ x A
	elab3gf.2	|- F/ x ps
	elab3gf.3	|- ( x = A -> ( ph <-> ps ) )
Assertion	elab3gf	|- ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		elab3gf.1	|- F/_ x A
2		elab3gf.2	|- F/ x ps
3		elab3gf.3	|- ( x = A -> ( ph <-> ps ) )
4	1 2 3	elabgf	|- ( A e. { x | ph } -> ( A e. { x | ph } <-> ps ) )
5	4	ibi	|- ( A e. { x | ph } -> ps )
6		pm2.21	|- ( -. ps -> ( ps -> A e. { x | ph } ) )
7	5 6	impbid2	|- ( -. ps -> ( A e. { x | ph } <-> ps ) )
8	1 2 3	elabgf	|- ( A e. B -> ( A e. { x | ph } <-> ps ) )
9	7 8	ja	|- ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) )