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
|- ( A. y e. x [. y / x ]. ph -> ph )
Assertion setinds
|- ph

Proof

Step Hyp Ref Expression
1 setinds.1
 |-  ( A. y e. x [. y / x ]. ph -> ph )
2 vex
 |-  x e. _V
3 setind
 |-  ( A. z ( z C_ { x | ph } -> z e. { x | ph } ) -> { x | ph } = _V )
4 dfss3
 |-  ( z C_ { x | ph } <-> A. y e. z y e. { x | ph } )
5 df-sbc
 |-  ( [. y / x ]. ph <-> y e. { x | ph } )
6 5 ralbii
 |-  ( A. y e. z [. y / x ]. ph <-> A. y e. z y e. { x | ph } )
7 nfcv
 |-  F/_ x z
8 nfsbc1v
 |-  F/ x [. y / x ]. ph
9 7 8 nfralw
 |-  F/ x A. y e. z [. y / x ]. ph
10 nfsbc1v
 |-  F/ x [. z / x ]. ph
11 9 10 nfim
 |-  F/ x ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph )
12 raleq
 |-  ( x = z -> ( A. y e. x [. y / x ]. ph <-> A. y e. z [. y / x ]. ph ) )
13 sbceq1a
 |-  ( x = z -> ( ph <-> [. z / x ]. ph ) )
14 12 13 imbi12d
 |-  ( x = z -> ( ( A. y e. x [. y / x ]. ph -> ph ) <-> ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) ) )
15 11 14 1 chvarfv
 |-  ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph )
16 6 15 sylbir
 |-  ( A. y e. z y e. { x | ph } -> [. z / x ]. ph )
17 4 16 sylbi
 |-  ( z C_ { x | ph } -> [. z / x ]. ph )
18 df-sbc
 |-  ( [. z / x ]. ph <-> z e. { x | ph } )
19 17 18 sylib
 |-  ( z C_ { x | ph } -> z e. { x | ph } )
20 3 19 mpg
 |-  { x | ph } = _V
21 20 eqcomi
 |-  _V = { x | ph }
22 21 abeq2i
 |-  ( x e. _V <-> ph )
23 2 22 mpbi
 |-  ph