Theorem setindtrs

Description: Set induction scheme without Infinity. See comments at setindtr . (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Hypotheses	setindtrs.a	|- ( A. y e. x ps -> ph )
	setindtrs.b	|- ( x = y -> ( ph <-> ps ) )
	setindtrs.c	|- ( x = B -> ( ph <-> ch ) )
Assertion	setindtrs	|- ( E. z ( Tr z /\ B e. z ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		setindtrs.a	|- ( A. y e. x ps -> ph )
2		setindtrs.b	|- ( x = y -> ( ph <-> ps ) )
3		setindtrs.c	|- ( x = B -> ( ph <-> ch ) )
4		setindtr	|- ( A. a ( a C_ { x | ph } -> a e. { x | ph } ) -> ( E. z ( Tr z /\ B e. z ) -> B e. { x | ph } ) )
5		dfss3	|- ( a C_ { x | ph } <-> A. y e. a y e. { x | ph } )
6		nfcv	|- F/_ x a
7		nfsab1	|- F/ x y e. { x | ph }
8	6 7	nfralw	|- F/ x A. y e. a y e. { x | ph }
9		nfsab1	|- F/ x a e. { x | ph }
10	8 9	nfim	|- F/ x ( A. y e. a y e. { x | ph } -> a e. { x | ph } )
11		raleq	|- ( x = a -> ( A. y e. x y e. { x | ph } <-> A. y e. a y e. { x | ph } ) )
12		eleq1w	|- ( x = a -> ( x e. { x | ph } <-> a e. { x | ph } ) )
13	11 12	imbi12d	|- ( x = a -> ( ( A. y e. x y e. { x | ph } -> x e. { x | ph } ) <-> ( A. y e. a y e. { x | ph } -> a e. { x | ph } ) ) )
14		vex	|- y e. _V
15	14 2	elab	|- ( y e. { x | ph } <-> ps )
16	15	ralbii	|- ( A. y e. x y e. { x | ph } <-> A. y e. x ps )
17		abid	|- ( x e. { x | ph } <-> ph )
18	1 16 17	3imtr4i	|- ( A. y e. x y e. { x | ph } -> x e. { x | ph } )
19	10 13 18	chvarfv	|- ( A. y e. a y e. { x | ph } -> a e. { x | ph } )
20	5 19	sylbi	|- ( a C_ { x | ph } -> a e. { x | ph } )
21	4 20	mpg	|- ( E. z ( Tr z /\ B e. z ) -> B e. { x | ph } )
22		elex	|- ( B e. z -> B e. _V )
23	22	adantl	|- ( ( Tr z /\ B e. z ) -> B e. _V )
24	23	exlimiv	|- ( E. z ( Tr z /\ B e. z ) -> B e. _V )
25	3	elabg	|- ( B e. _V -> ( B e. { x | ph } <-> ch ) )
26	24 25	syl	|- ( E. z ( Tr z /\ B e. z ) -> ( B e. { x | ph } <-> ch ) )
27	21 26	mpbid	|- ( E. z ( Tr z /\ B e. z ) -> ch )