Theorem tfis2f

Description: Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994)

	Ref	Expression
Hypotheses	tfis2f.1	$$⊢Ⅎx\psi$$
	tfis2f.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	tfis2f.3	$$⊢x\in \mathrm{On}\to \left(\forall y\in x\psi \to \phi \right)$$
Assertion	tfis2f	$$⊢x\in \mathrm{On}\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		tfis2f.1	$$⊢Ⅎx\psi$$
2		tfis2f.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		tfis2f.3	$$⊢x\in \mathrm{On}\to \left(\forall y\in x\psi \to \phi \right)$$
4	1 2	sbiev	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
5	4	ralbii	$$⊢\forall y\in x\left[y/x\right]\phi \leftrightarrow \forall y\in x\psi$$
6	5 3	biimtrid	$$⊢x\in \mathrm{On}\to \left(\forall y\in x\left[y/x\right]\phi \to \phi \right)$$
7	6	tfis	$$⊢x\in \mathrm{On}\to \phi$$