Theorem intab 3635

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). (Contributed by NM, 28-Jul-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)

Hypotheses

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

Assertion

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

Distinct variable groups:   x,A   ph,x   x,y

Allowed substitution hints:   ph(y)   A(y)

Proof of Theorem intab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2043	. . . . . . . . . 10 |- (z = x -> (z = A <-> x = A))
2	1	anbi2d 437	. . . . . . . . 9 |- (z = x -> ((ph /\ z = A) <-> (ph /\ x = A)))
3	2	exbidv 1703	. . . . . . . 8 |- (z = x -> (E.y(ph /\ z = A) <-> E.y(ph /\ x = A)))
4	3	cbvabv 2158	. . . . . . 7 |- {z | E.y(ph /\ z = A) } = {x | E.y(ph /\ x = A) }
5		intab.2	. . . . . . 7 |- {x | E.y(ph /\ x = A) } e. _V
6	4, 5	eqeltri 2107	. . . . . 6 |- {z | E.y(ph /\ z = A) } e. _V
7		nfe1 1382	. . . . . . . . 9 |- F/yE.y(ph /\ z = A)
8	7	nfab 2179	. . . . . . . 8 |- F/_y {z | E.y(ph /\ z = A) }
9	8	nfeq2 2186	. . . . . . 7 |- F/y x = {z | E.y(ph /\ z = A) }
10		eleq2 2098	. . . . . . . 8 |- (x = {z | E.y(ph /\ z = A) } -> (A e. x <-> A e. {z | E.y(ph /\ z = A) }))
11	10	imbi2d 219	. . . . . . 7 |- (x = {z | E.y(ph /\ z = A) } -> ((ph -> A e. x) <-> (ph -> A e. {z | E.y(ph /\ z = A) })))
12	9, 11	albid 1503	. . . . . 6 |- (x = {z | E.y(ph /\ z = A) } -> (A.y(ph -> A e. x) <-> A.y(ph -> A e. {z | E.y(ph /\ z = A) })))
13	6, 12	elab 2681	. . . . 5 |- ( {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) }))
14		19.8a 1479	. . . . . . . . 9 |- ((ph /\ z = A) -> E.y(ph /\ z = A))
15	14	ex 108	. . . . . . . 8 |- (ph -> (z = A -> E.y(ph /\ z = A)))
16	15	alrimiv 1751	. . . . . . 7 |- (ph -> A.z(z = A -> E.y(ph /\ z = A)))
17		intab.1	. . . . . . . 8 |- A e. _V
18	17	sbc6 2783	. . . . . . 7 |- ( [.A / z ].E.y(ph /\ z = A) <-> A.z(z = A -> E.y(ph /\ z = A)))
19	16, 18	sylibr 137	. . . . . 6 |- (ph -> [.A / z ].E.y(ph /\ z = A))
20		df-sbc 2759	. . . . . 6 |- ( [.A / z ].E.y(ph /\ z = A) <-> A e. {z | E.y(ph /\ z = A) })
21	19, 20	sylib 127	. . . . 5 |- (ph -> A e. {z | E.y(ph /\ z = A) })
22	13, 21	mpgbir 1339	. . . 4 |- {z | E.y(ph /\ z = A) } e. {x | A.y(ph -> A e. x) }
23		intss1 3621	. . . 4 |- ( {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 7	. . 3 |- |^| {x | A.y(ph -> A e. x) } C_ {z | E.y(ph /\ z = A) }
25		19.29r 1509	. . . . . . . 8 |- ((E.y(ph /\ z = A) /\ A.y(ph -> A e. x)) -> E.y((ph /\ z = A) /\ (ph -> A e. x)))
26		simplr 482	. . . . . . . . . 10 |- (((ph /\ z = A) /\ (ph -> A e. x)) -> z = A)
27		pm3.35 329	. . . . . . . . . . 11 |- ((ph /\ (ph -> A e. x)) -> A e. x)
28	27	adantlr 446	. . . . . . . . . 10 |- (((ph /\ z = A) /\ (ph -> A e. x)) -> A e. x)
29	26, 28	eqeltrd 2111	. . . . . . . . 9 |- (((ph /\ z = A) /\ (ph -> A e. x)) -> z e. x)
30	29	exlimiv 1486	. . . . . . . 8 |- (E.y((ph /\ z = A) /\ (ph -> A e. x)) -> z e. x)
31	25, 30	syl 14	. . . . . . 7 |- ((E.y(ph /\ z = A) /\ A.y(ph -> A e. x)) -> z e. x)
32	31	ex 108	. . . . . 6 |- (E.y(ph /\ z = A) -> (A.y(ph -> A e. x) -> z e. x))
33	32	alrimiv 1751	. . . . 5 |- (E.y(ph /\ z = A) -> A.x(A.y(ph -> A e. x) -> z e. x))
34		vex 2554	. . . . . 6 |- z e. _V
35	34	elintab 3617	. . . . 5 |- (z e. |^| {x | A.y(ph -> A e. x) } <-> A.x(A.y(ph -> A e. x) -> z e. x))
36	33, 35	sylibr 137	. . . 4 |- (E.y(ph /\ z = A) -> z e. |^| {x | A.y(ph -> A e. x) })
37	36	abssi 3009	. . 3 |- {z | E.y(ph /\ z = A) } C_ |^| {x | A.y(ph -> A e. x) }
38	24, 37	eqssi 2955	. 2 |- |^| {x | A.y(ph -> A e. x) } = {z | E.y(ph /\ z = A) }
39	38, 4	eqtri 2057	1 |- |^| {x | A.y(ph -> A e. x) } = {x | E.y(ph /\ x = A) }

Syntax hints:   -> wi 4   /\ wa 97  A.wal 1240   = wceq 1242  E.wex 1378   e. wcel 1390   {cab 2023   _Vcvv 2551   [.wsbc 2758   C_ wss 2911   |^|cint 3606

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-sbc 2759  df-in 2918  df-ss 2925  df-int 3607

This theorem is referenced by: (None)