Theorem elrabf

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003)

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

Proof

Step	Hyp	Ref	Expression
1		elrabf.1	|- F/_ x A
2		elrabf.2	|- F/_ x B
3		elrabf.3	|- F/ x ps
4		elrabf.4	|- ( x = A -> ( ph <-> ps ) )
5		elex	|- ( A e. { x e. B | ph } -> A e. _V )
6		elex	|- ( A e. B -> A e. _V )
7	6	adantr	|- ( ( A e. B /\ ps ) -> A e. _V )
8		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
9	8	eleq2i	|- ( A e. { x e. B | ph } <-> A e. { x | ( x e. B /\ ph ) } )
10	1 2	nfel	|- F/ x A e. B
11	10 3	nfan	|- F/ x ( A e. B /\ ps )
12		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
13	12 4	anbi12d	|- ( x = A -> ( ( x e. B /\ ph ) <-> ( A e. B /\ ps ) ) )
14	1 11 13	elabgf	|- ( A e. _V -> ( A e. { x | ( x e. B /\ ph ) } <-> ( A e. B /\ ps ) ) )
15	9 14	bitrid	|- ( A e. _V -> ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) ) )
16	5 7 15	pm5.21nii	|- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )