Metamath Proof Explorer


Theorem frpoins2fg

Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022)

Ref Expression
Hypotheses frpoins2fg.1 y A z Pred R A y ψ φ
frpoins2fg.2 y ψ
frpoins2fg.3 y = z φ ψ
Assertion frpoins2fg R Fr A R Po A R Se A y A φ

Proof

Step Hyp Ref Expression
1 frpoins2fg.1 y A z Pred R A y ψ φ
2 frpoins2fg.2 y ψ
3 frpoins2fg.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 1 adantl R Fr A R Po A R Se A y A z Pred R A y ψ φ
9 7 8 syl5bi R Fr A R Po A R Se A y A z Pred R A y [˙z / y]˙ φ φ
10 9 frpoinsg R Fr A R Po A R Se A y A φ