Metamath Proof Explorer


Theorem frins

Description: Well-Founded Induction Schema. If a property passes from all elements less than y of a well-founded class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses frins.1 R Fr A
frins.2 R Se A
frins.3 y A z Pred R A y [˙z / y]˙ φ φ
Assertion frins y A φ

Proof

Step Hyp Ref Expression
1 frins.1 R Fr A
2 frins.2 R Se A
3 frins.3 y A z Pred R A y [˙z / y]˙ φ φ
4 3 frinsg R Fr A R Se A y A φ
5 1 2 4 mp2an y A φ
6 5 rspec y A φ