Theorem setinds2

Description: _E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011)

	Ref	Expression
Hypotheses	setinds2.1	|- ( x = y -> ( ph <-> ps ) )
	setinds2.2	|- ( A. y e. x ps -> ph )
Assertion	setinds2	|- ph

Proof

Step	Hyp	Ref	Expression
1		setinds2.1	|- ( x = y -> ( ph <-> ps ) )
2		setinds2.2	|- ( A. y e. x ps -> ph )
3		nfv	|- F/ x ps
4	3 1 2	setinds2f	|- ph