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	syl5bi	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
7	6	tfis	⊢ ( 𝑥 ∈ On → 𝜑 )