Theorem intab

Description: The intersection of a special case of a class abstraction. y may be free in ph and A , which can be thought of a ph ( y ) and A ( y ) . Typically, abrexex2 or abexssex can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006) (Proof shortened by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Hypotheses	intab.1	|- A e. _V
	intab.2	|- { x | E. y ( ph /\ x = A ) } e. _V
Assertion	intab	|- |^| { x | A. y ( ph -> A e. x ) } = { x | E. y ( ph /\ x = A ) }

Proof

Step	Hyp	Ref	Expression
1		intab.1	|- A e. _V
2		intab.2	|- { x | E. y ( ph /\ x = A ) } e. _V
3		eqeq1	|- ( z = x -> ( z = A <-> x = A ) )
4	3	anbi2d	|- ( z = x -> ( ( ph /\ z = A ) <-> ( ph /\ x = A ) ) )
5	4	exbidv	|- ( z = x -> ( E. y ( ph /\ z = A ) <-> E. y ( ph /\ x = A ) ) )
6	5	cbvabv	|- { z | E. y ( ph /\ z = A ) } = { x | E. y ( ph /\ x = A ) }
7	6 2	eqeltri	|- { z | E. y ( ph /\ z = A ) } e. _V
8		nfe1	|- F/ y E. y ( ph /\ z = A )
9	8	nfab	|- F/_ y { z | E. y ( ph /\ z = A ) }
10	9	nfeq2	|- F/ y x = { z | E. y ( ph /\ z = A ) }
11		eleq2	|- ( x = { z | E. y ( ph /\ z = A ) } -> ( A e. x <-> A e. { z | E. y ( ph /\ z = A ) } ) )
12	11	imbi2d	|- ( x = { z | E. y ( ph /\ z = A ) } -> ( ( ph -> A e. x ) <-> ( ph -> A e. { z | E. y ( ph /\ z = A ) } ) ) )
13	10 12	albid	|- ( x = { z | E. y ( ph /\ z = A ) } -> ( A. y ( ph -> A e. x ) <-> A. y ( ph -> A e. { z | E. y ( ph /\ z = A ) } ) ) )
14	7 13	elab	|- ( { z | E. y ( ph /\ z = A ) } e. { x | A. y ( ph -> A e. x ) } <-> A. y ( ph -> A e. { z | E. y ( ph /\ z = A ) } ) )
15		19.8a	|- ( ( ph /\ z = A ) -> E. y ( ph /\ z = A ) )
16	15	ex	|- ( ph -> ( z = A -> E. y ( ph /\ z = A ) ) )
17	16	alrimiv	|- ( ph -> A. z ( z = A -> E. y ( ph /\ z = A ) ) )
18	1	sbc6	|- ( [. A / z ]. E. y ( ph /\ z = A ) <-> A. z ( z = A -> E. y ( ph /\ z = A ) ) )
19	17 18	sylibr	|- ( ph -> [. A / z ]. E. y ( ph /\ z = A ) )
20		df-sbc	|- ( [. A / z ]. E. y ( ph /\ z = A ) <-> A e. { z | E. y ( ph /\ z = A ) } )
21	19 20	sylib	|- ( ph -> A e. { z | E. y ( ph /\ z = A ) } )
22	14 21	mpgbir	|- { z | E. y ( ph /\ z = A ) } e. { x | A. y ( ph -> A e. x ) }
23		intss1	|- ( { z | E. y ( ph /\ z = A ) } e. { x | A. y ( ph -> A e. x ) } -> |^| { x | A. y ( ph -> A e. x ) } C_ { z | E. y ( ph /\ z = A ) } )
24	22 23	ax-mp	|- |^| { x | A. y ( ph -> A e. x ) } C_ { z | E. y ( ph /\ z = A ) }
25		19.29r	|- ( ( E. y ( ph /\ z = A ) /\ A. y ( ph -> A e. x ) ) -> E. y ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) )
26		simplr	|- ( ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> z = A )
27		pm3.35	|- ( ( ph /\ ( ph -> A e. x ) ) -> A e. x )
28	27	adantlr	|- ( ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> A e. x )
29	26 28	eqeltrd	|- ( ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> z e. x )
30	29	exlimiv	|- ( E. y ( ( ph /\ z = A ) /\ ( ph -> A e. x ) ) -> z e. x )
31	25 30	syl	|- ( ( E. y ( ph /\ z = A ) /\ A. y ( ph -> A e. x ) ) -> z e. x )
32	31	ex	|- ( E. y ( ph /\ z = A ) -> ( A. y ( ph -> A e. x ) -> z e. x ) )
33	32	alrimiv	|- ( E. y ( ph /\ z = A ) -> A. x ( A. y ( ph -> A e. x ) -> z e. x ) )
34		vex	|- z e. _V
35	34	elintab	|- ( z e. |^| { x | A. y ( ph -> A e. x ) } <-> A. x ( A. y ( ph -> A e. x ) -> z e. x ) )
36	33 35	sylibr	|- ( E. y ( ph /\ z = A ) -> z e. |^| { x | A. y ( ph -> A e. x ) } )
37	36	abssi	|- { z | E. y ( ph /\ z = A ) } C_ |^| { x | A. y ( ph -> A e. x ) }
38	24 37	eqssi	|- |^| { x | A. y ( ph -> A e. x ) } = { z | E. y ( ph /\ z = A ) }
39	38 6	eqtri	|- |^| { x | A. y ( ph -> A e. x ) } = { x | E. y ( ph /\ x = A ) }