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

Metamath Proof Explorer

Theorem frins2

Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 8-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	frins2.1	$⊢ y \in A \to (\forall z \in Pred (R, A, y) ψ \to φ)$
	frins2.3	$⊢ y = z \to (φ \leftrightarrow ψ)$
Assertion	frins2	$⊢ (R Fr A \land R Se A) \to \forall y \in A φ$

Proof

Step	Hyp	Ref	Expression
1		frins2.1	$⊢ y \in A \to (\forall z \in Pred (R, A, y) ψ \to φ)$
2		frins2.3	$⊢ y = z \to (φ \leftrightarrow ψ)$
3		nfv	$⊢ Ⅎ y ψ$
4	1 3 2	frins2f	$⊢ (R Fr A \land R Se A) \to \forall y \in A φ$