Metamath Proof Explorer


Theorem frpoins2g

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

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

Proof

Step Hyp Ref Expression
1 frpoins2g.1 y A z Pred R A y ψ φ
2 frpoins2g.3 y = z φ ψ
3 nfv y ψ
4 1 3 2 frpoins2fg R Fr A R Po A R Se A y A φ