Metamath Proof Explorer

Theorem tfis2d

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

Ref Expression
Hypotheses tfis2d.1 ⊢ φ → x = y → ψ ↔ χ
tfis2d.2 ⊢ φ → x ∈ On → ∀ y ∈ x χ → ψ
Assertion tfis2d ⊢ φ → x ∈ On → ψ

Proof

Step Hyp Ref Expression
1 tfis2d.1 ⊢ φ → x = y → ψ ↔ χ
2 tfis2d.2 ⊢ φ → x ∈ On → ∀ y ∈ x χ → ψ
3 1 com12 ⊢ x = y → φ → ψ ↔ χ
4 3 pm5.74d ⊢ x = y → φ → ψ ↔ φ → χ
5 r19.21v ⊢ ∀ y ∈ x φ → χ ↔ φ → ∀ y ∈ x χ
6 2 com12 ⊢ x ∈ On → φ → ∀ y ∈ x χ → ψ
7 6 a2d ⊢ x ∈ On → φ → ∀ y ∈ x χ → φ → ψ
8 5 7 biimtrid ⊢ x ∈ On → ∀ y ∈ x φ → χ → φ → ψ
9 4 8 tfis2 ⊢ x ∈ On → φ → ψ
10 9 com12 ⊢ φ → x ∈ On → ψ