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

Metamath Proof Explorer

Theorem tfis2f

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

Ref Expression
Hypotheses tfis2f.1 ⊢ Ⅎ 𝑥 𝜓
tfis2f.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
tfis2f.3 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 ) )
Assertion tfis2f ( 𝑥 ∈ On → 𝜑 )

Proof

Step Hyp Ref Expression
1 tfis2f.1 ⊢ Ⅎ 𝑥 𝜓
2 tfis2f.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3 tfis2f.3 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝜓 → 𝜑 ) )
4 1 2 sbiev ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
5 4 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝑥 𝜓 )
6 5 3 biimtrid ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
7 6 tfis ⊢ ( 𝑥 ∈ On → 𝜑 )