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 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
tfis3.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
tfis3.3 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 ) )
Assertion tfis3 ( 𝐴 ∈ On → 𝜒 )

Proof

Step Hyp Ref Expression
1 tfis3.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 tfis3.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
3 tfis3.3 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 ) )
4 1 3 tfis2 ⊢ ( 𝑥 ∈ On → 𝜑 )
5 2 4 vtoclga ⊢ ( 𝐴 ∈ On → 𝜒 )