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

Metamath Proof Explorer

Theorem frpoins3g

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

	Ref	Expression
Hypotheses	frpoins3g.1	$⊢ x \in A \to (\forall y \in Pred (R, A, x) ψ \to φ)$
	frpoins3g.2	$⊢ x = y \to (φ \leftrightarrow ψ)$
	frpoins3g.3	$⊢ x = B \to (φ \leftrightarrow χ)$
Assertion	frpoins3g	$⊢ ((R Fr A \land R Po A \land R Se A) \land B \in A) \to χ$

Step	Hyp	Ref	Expression
1		frpoins3g.1	$⊢ x \in A \to (\forall y \in Pred (R, A, x) ψ \to φ)$
2		frpoins3g.2	$⊢ x = y \to (φ \leftrightarrow ψ)$
3		frpoins3g.3	$⊢ x = B \to (φ \leftrightarrow χ)$
4	1 2	frpoins2g	$⊢ (R Fr A \land R Po A \land R Se A) \to \forall x \in A φ$
5	3	rspccva	$⊢ (\forall x \in A φ \land B \in A) \to χ$
6	4 5	sylan	$⊢ ((R Fr A \land R Po A \land R Se A) \land B \in A) \to χ$