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φψ
tfis2.2 xOnyxψφ
Assertion tfis2 xOnφ

Proof

Step Hyp Ref Expression
1 tfis2.1 x=yφψ
2 tfis2.2 xOnyxψφ
3 nfv xψ
4 3 1 2 tfis2f xOnφ