Theorem setinds2f

Description: _E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011) (Revised by Mario Carneiro, 11-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		setinds2f.1	|- F/ x ps
2		setinds2f.2	|- ( x = y -> ( ph <-> ps ) )
3		setinds2f.3	|- ( A. y e. x ps -> ph )
4		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
5	1 2	sbiev	|- ( [ y / x ] ph <-> ps )
6	4 5	bitr3i	|- ( [. y / x ]. ph <-> ps )
7	6	ralbii	|- ( A. y e. x [. y / x ]. ph <-> A. y e. x ps )
8	7 3	sylbi	|- ( A. y e. x [. y / x ]. ph -> ph )
9	8	setinds	|- ph