This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tfis3

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

Ref Expression
Hypotheses tfis3.1 ⊢ x = y → φ ↔ ψ
tfis3.2 ⊢ x = A → φ ↔ χ
tfis3.3 ⊢ x ∈ On → ∀ y ∈ x ψ → φ
Assertion tfis3 ⊢ A ∈ On → χ

Proof

Step Hyp Ref Expression
1 tfis3.1 ⊢ x = y → φ ↔ ψ
2 tfis3.2 ⊢ x = A → φ ↔ χ
3 tfis3.3 ⊢ x ∈ On → ∀ y ∈ x ψ → φ
4 1 3 tfis2 ⊢ x ∈ On → φ
5 2 4 vtoclga ⊢ A ∈ On → χ