Theorem bnj157

Description: Well-founded induction restricted to a set ( A e. _V ). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj157.1	$$⊢\psi \leftrightarrow \forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
	bnj157.2	$$⊢A\in \mathrm{V}$$
	bnj157.3	$$⊢R\mathrm{Fr}A$$
Assertion	bnj157	$$⊢\forall x\in A\left(\psi \to \phi \right)\to \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		bnj157.1	$$⊢\psi \leftrightarrow \forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
2		bnj157.2	$$⊢A\in \mathrm{V}$$
3		bnj157.3	$$⊢R\mathrm{Fr}A$$
4	2 1	bnj110	$$⊢\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\to \forall x\in A\phi$$
5	3 4	mpan	$$⊢\forall x\in A\left(\psi \to \phi \right)\to \forall x\in A\phi$$