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	$$⊢Ⅎx\psi$$
	setinds2f.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	setinds2f.3	$$⊢\forall y\in x\psi \to \phi$$
Assertion	setinds2f	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		setinds2f.1	$$⊢Ⅎx\psi$$
2		setinds2f.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		setinds2f.3	$$⊢\forall y\in x\psi \to \phi$$
4		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
5	1 2	sbiev	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
6	4 5	bitr3i	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
7	6	ralbii	$$⊢\forall y\in x\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \forall y\in x\psi$$
8	7 3	sylbi	$$⊢\forall y\in x\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \phi$$
9	8	setinds	$$⊢\phi$$