Theorem tfis2

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

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

Proof

Step	Hyp	Ref	Expression
1		tfis2.1	|- ( x = y -> ( ph <-> ps ) )
2		tfis2.2	|- ( x e. On -> ( A. y e. x ps -> ph ) )
3		nfv	|- F/ x ps
4	3 1 2	tfis2f	|- ( x e. On -> ph )