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 → 𝜒 )