Theorem setinds

Description: Principle of set induction (or _E -induction). If a property passes from all elements of x to x itself, then it holds for all x . (Contributed by Scott Fenton, 10-Mar-2011)

	Ref	Expression
Hypothesis	setinds.1	$$⊢\forall y\in x\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \phi$$
Assertion	setinds	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		setinds.1	$$⊢\forall y\in x\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \phi$$
2		vex	$$⊢x\in \mathrm{V}$$
3		setind	$$⊢\forall z\left(z\subseteq \left\{x|\phi \right\}\to z\in \left\{x|\phi \right\}\right)\to \left\{x|\phi \right\}=\mathrm{V}$$
4		dfss3	$$⊢z\subseteq \left\{x|\phi \right\}\leftrightarrow \forall y\in zy\in \left\{x|\phi \right\}$$
5		df-sbc	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow y\in \left\{x|\phi \right\}$$
6	5	ralbii	$$⊢\forall y\in z\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \forall y\in zy\in \left\{x|\phi \right\}$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
8		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
9	7 8	nfralw	$$⊢Ⅎx\forall y\in z\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
10		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
11	9 10	nfim	$$⊢Ⅎx\left(\forall y\in z\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
12		raleq	$$⊢x=z\to \left(\forall y\in x\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \forall y\in z\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
13		sbceq1a	$$⊢x=z\to \left(\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
14	12 13	imbi12d	$$⊢x=z\to \left(\left(\forall y\in x\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \phi \right)\leftrightarrow \left(\forall y\in z\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\right)$$
15	11 14 1	chvarfv	$$⊢\forall y\in z\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
16	6 15	sylbir	$$⊢\forall y\in zy\in \left\{x|\phi \right\}\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
17	4 16	sylbi	$$⊢z\subseteq \left\{x|\phi \right\}\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
18		df-sbc	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow z\in \left\{x|\phi \right\}$$
19	17 18	sylib	$$⊢z\subseteq \left\{x|\phi \right\}\to z\in \left\{x|\phi \right\}$$
20	3 19	mpg	$$⊢\left\{x|\phi \right\}=\mathrm{V}$$
21	20	eqcomi	$$⊢\mathrm{V}=\left\{x|\phi \right\}$$
22	21	abeq2i	$$⊢x\in \mathrm{V}\leftrightarrow \phi$$
23	2 22	mpbi	$$⊢\phi$$