This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqabri 
 |-  ( x e. _V <-> ph )
23 2 22 mpbi 
 |-  ph