Metamath Proof Explorer


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 )