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

Metamath Proof Explorer

Theorem frins2f

Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2011) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses frins2f.1 ⊢ y ∈ A → ∀ z ∈ Pred R A y ψ → φ
frins2f.2 ⊢ Ⅎ y ψ
frins2f.3 ⊢ y = z → φ ↔ ψ
Assertion frins2f ⊢ R Fr A ∧ R Se A → ∀ y ∈ A φ

Proof

Step Hyp Ref Expression
1 frins2f.1 ⊢ y ∈ A → ∀ z ∈ Pred R A y ψ → φ
2 frins2f.2 ⊢ Ⅎ y ψ
3 frins2f.3 ⊢ y = z → φ ↔ ψ
4 sbsbc ⊢ z y φ ↔ [˙z / y]˙ φ
5 2 3 sbiev ⊢ z y φ ↔ ψ
6 4 5 bitr3i ⊢ [˙z / y]˙ φ ↔ ψ
7 6 ralbii ⊢ ∀ z ∈ Pred R A y [˙z / y]˙ φ ↔ ∀ z ∈ Pred R A y ψ
8 7 1 biimtrid ⊢ y ∈ A → ∀ z ∈ Pred R A y [˙z / y]˙ φ → φ
9 8 frinsg ⊢ R Fr A ∧ R Se A → ∀ y ∈ A φ