Metamath Proof Explorer


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 ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 )
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 abeq2i ( 𝑥 ∈ V ↔ 𝜑 )
23 2 22 mpbi 𝜑