Theorem elabgf

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of Quine p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003) (Revised by Mario Carneiro, 12-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		elabgf.1	|- F/_ x A
2		elabgf.2	|- F/ x ps
3		elabgf.3	|- ( x = A -> ( ph <-> ps ) )
4		nfab1	|- F/_ x { x | ph }
5	1 4	nfel	|- F/ x A e. { x | ph }
6	5 2	nfbi	|- F/ x ( A e. { x | ph } <-> ps )
7		eleq1	|- ( x = A -> ( x e. { x | ph } <-> A e. { x | ph } ) )
8	7 3	bibi12d	|- ( x = A -> ( ( x e. { x | ph } <-> ph ) <-> ( A e. { x | ph } <-> ps ) ) )
9		abid	|- ( x e. { x | ph } <-> ph )
10	1 6 8 9	vtoclgf	|- ( A e. B -> ( A e. { x | ph } <-> ps ) )