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

Metamath Proof Explorer

Theorem wfis2g

Description: Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011)

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

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