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	⊢ ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 )
	Assertion	setinds	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		setinds.1	⊢ ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 )
2		vex	⊢ 𝑥 ∈ V
3		setind	⊢ ( ∀ 𝑧 ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) → { 𝑥 ∣ 𝜑 } = V )
4		dfss3	⊢ ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑧 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
5		df-sbc	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
6	5	ralbii	⊢ ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝑧 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
7		nfcv	⊢ Ⅎ 𝑥 𝑧
8		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
9	7 8	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑
10		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
11	9 10	nfim	⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 )
12		raleq	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 ) )
13		sbceq1a	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
14	12 13	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) ↔ ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
15	11 14 1	chvarfv	⊢ ( ∀ 𝑦 ∈ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 )
16	6 15	sylbir	⊢ ( ∀ 𝑦 ∈ 𝑧 𝑦 ∈ { 𝑥 ∣ 𝜑 } → [ 𝑧 / 𝑥 ] 𝜑 )
17	4 16	sylbi	⊢ ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } → [ 𝑧 / 𝑥 ] 𝜑 )
18		df-sbc	⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 ∈ { 𝑥 ∣ 𝜑 } )
19	17 18	sylib	⊢ ( 𝑧 ⊆ { 𝑥 ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∣ 𝜑 } )
20	3 19	mpg	⊢ { 𝑥 ∣ 𝜑 } = V
21	20	eqcomi	⊢ V = { 𝑥 ∣ 𝜑 }
22	21	eqabri	⊢ ( 𝑥 ∈ V ↔ 𝜑 )
23	2 22	mpbi	⊢ 𝜑

Metamath Proof Explorer

Theorem setinds

Proof