Theorem tfis3

Description: Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003)

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

Proof

Step	Hyp	Ref	Expression
1		tfis3.1	|- ( x = y -> ( ph <-> ps ) )
2		tfis3.2	|- ( x = A -> ( ph <-> ch ) )
3		tfis3.3	|- ( x e. On -> ( A. y e. x ps -> ph ) )
4	1 3	tfis2	|- ( x e. On -> ph )
5	2 4	vtoclga	|- ( A e. On -> ch )