Theorem tfis2f

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

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

Proof

Step	Hyp	Ref	Expression
1		tfis2f.1	|- F/ x ps
2		tfis2f.2	|- ( x = y -> ( ph <-> ps ) )
3		tfis2f.3	|- ( x e. On -> ( A. y e. x ps -> ph ) )
4	1 2	sbiev	|- ( [ y / x ] ph <-> ps )
5	4	ralbii	|- ( A. y e. x [ y / x ] ph <-> A. y e. x ps )
6	5 3	syl5bi	|- ( x e. On -> ( A. y e. x [ y / x ] ph -> ph ) )
7	6	tfis	|- ( x e. On -> ph )