Metamath Proof Explorer

Theorem setind

Description: Set (epsilon) induction. Theorem 5.22 of TakeutiZaring p. 21. (Contributed by NM, 17-Sep-2003)

Ref Expression
Assertion setind 
|- ( A. x ( x C_ A -> x e. A ) -> A = _V )

Proof

Step Hyp Ref Expression
1 ssindif0 
 |-  ( y C_ A <-> ( y i^i ( _V \ A ) ) = (/) )
2 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
3 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
4 2 3 imbi12d 
 |-  ( x = y -> ( ( x C_ A -> x e. A ) <-> ( y C_ A -> y e. A ) ) )
5 4 spvv 
 |-  ( A. x ( x C_ A -> x e. A ) -> ( y C_ A -> y e. A ) )
6 1 5 biimtrrid 
 |-  ( A. x ( x C_ A -> x e. A ) -> ( ( y i^i ( _V \ A ) ) = (/) -> y e. A ) )
7 eldifn 
 |-  ( y e. ( _V \ A ) -> -. y e. A )
8 6 7 nsyli 
 |-  ( A. x ( x C_ A -> x e. A ) -> ( y e. ( _V \ A ) -> -. ( y i^i ( _V \ A ) ) = (/) ) )
9 8 imp 
 |-  ( ( A. x ( x C_ A -> x e. A ) /\ y e. ( _V \ A ) ) -> -. ( y i^i ( _V \ A ) ) = (/) )
10 9 nrexdv 
 |-  ( A. x ( x C_ A -> x e. A ) -> -. E. y e. ( _V \ A ) ( y i^i ( _V \ A ) ) = (/) )
11 zfregs 
 |-  ( ( _V \ A ) =/= (/) -> E. y e. ( _V \ A ) ( y i^i ( _V \ A ) ) = (/) )
12 11 necon1bi 
 |-  ( -. E. y e. ( _V \ A ) ( y i^i ( _V \ A ) ) = (/) -> ( _V \ A ) = (/) )
13 10 12 syl 
 |-  ( A. x ( x C_ A -> x e. A ) -> ( _V \ A ) = (/) )
14 vdif0 
 |-  ( A = _V <-> ( _V \ A ) = (/) )
15 13 14 sylibr 
 |-  ( A. x ( x C_ A -> x e. A ) -> A = _V )