Theorem tfis2d

Description: Transfinite Induction Schema, using implicit substitution. (Contributed by Emmett Weisz, 3-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		tfis2d.1	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
2		tfis2d.2	⊢ ( 𝜑 → ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜓 ) ) )
3	1	com12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) )
4	3	pm5.74d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
5		r19.21v	⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝜑 → 𝜒 ) ↔ ( 𝜑 → ∀ 𝑦 ∈ 𝑥 𝜒 ) )
6	2	com12	⊢ ( 𝑥 ∈ On → ( 𝜑 → ( ∀ 𝑦 ∈ 𝑥 𝜒 → 𝜓 ) ) )
7	6	a2d	⊢ ( 𝑥 ∈ On → ( ( 𝜑 → ∀ 𝑦 ∈ 𝑥 𝜒 ) → ( 𝜑 → 𝜓 ) ) )
8	5 7	syl5bi	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝜑 → 𝜒 ) → ( 𝜑 → 𝜓 ) ) )
9	4 8	tfis2	⊢ ( 𝑥 ∈ On → ( 𝜑 → 𝜓 ) )
10	9	com12	⊢ ( 𝜑 → ( 𝑥 ∈ On → 𝜓 ) )