Theorem intab 3957

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 in set.mm or abexssex in set.mm can be used to satisfy the second hypothesis. (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 2359	. . . . . . . . . 10 |- (z = x -> (z = A <-> x = A))
2	1	anbi2d 684	. . . . . . . . 9 |- (z = x -> ((ph /\ z = A) <-> (ph /\ x = A)))
3	2	exbidv 1626	. . . . . . . 8 |- (z = x -> (E.y(ph /\ z = A) <-> E.y(ph /\ x = A)))
4	3	cbvabv 2473	. . . . . . 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 2423	. . . . . 6 |- {z | E.y(ph /\ z = A)} e. _V
7		nfe1 1732	. . . . . . . . 9 |- F/yE.y(ph /\ z = A)
8	7	nfab 2494	. . . . . . . 8 |- F/_y{z | E.y(ph /\ z = A)}
9	8	nfeq2 2501	. . . . . . 7 |- F/y x = {z | E.y(ph /\ z = A)}
10		eleq2 2414	. . . . . . . 8 |- (x = {z | E.y(ph /\ z = A)} -> (A e. x <-> A e. {z | E.y(ph /\ z = A)}))
11	10	imbi2d 307	. . . . . . 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 1772	. . . . . 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 2986	. . . . 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 1756	. . . . . . . . 9 |- ((ph /\ z = A) -> E.y(ph /\ z = A))
15	14	ex 423	. . . . . . . 8 |- (ph -> (z = A -> E.y(ph /\ z = A)))
16	15	alrimiv 1631	. . . . . . 7 |- (ph -> A.z(z = A -> E.y(ph /\ z = A)))
17		intab.1	. . . . . . . 8 |- A e. _V
18	17	sbc6 3073	. . . . . . 7 |- ( [.A / z ].E.y(ph /\ z = A) <-> A.z(z = A -> E.y(ph /\ z = A)))
19	16, 18	sylibr 203	. . . . . 6 |- (ph -> [.A / z ].E.y(ph /\ z = A))
20		df-sbc 3048	. . . . . 6 |- ( [.A / z ].E.y(ph /\ z = A) <-> A e. {z | E.y(ph /\ z = A)})
21	19, 20	sylib 188	. . . . 5 |- (ph -> A e. {z | E.y(ph /\ z = A)})
22	13, 21	mpgbir 1550	. . . 4 |- {z | E.y(ph /\ z = A)} e. {x | A.y(ph -> A e. x)}
23		intss1 3942	. . . 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 5	. . 3 |- |^|{x | A.y(ph -> A e. x)} C_ {z | E.y(ph /\ z = A)}
25		19.29r 1597	. . . . . . . 8 |- ((E.y(ph /\ z = A) /\ A.y(ph -> A e. x)) -> E.y((ph /\ z = A) /\ (ph -> A e. x)))
26		simplr 731	. . . . . . . . . 10 |- (((ph /\ z = A) /\ (ph -> A e. x)) -> z = A)
27		pm3.35 570	. . . . . . . . . . 11 |- ((ph /\ (ph -> A e. x)) -> A e. x)
28	27	adantlr 695	. . . . . . . . . 10 |- (((ph /\ z = A) /\ (ph -> A e. x)) -> A e. x)
29	26, 28	eqeltrd 2427	. . . . . . . . 9 |- (((ph /\ z = A) /\ (ph -> A e. x)) -> z e. x)
30	29	exlimiv 1634	. . . . . . . 8 |- (E.y((ph /\ z = A) /\ (ph -> A e. x)) -> z e. x)
31	25, 30	syl 15	. . . . . . 7 |- ((E.y(ph /\ z = A) /\ A.y(ph -> A e. x)) -> z e. x)
32	31	ex 423	. . . . . 6 |- (E.y(ph /\ z = A) -> (A.y(ph -> A e. x) -> z e. x))
33	32	alrimiv 1631	. . . . 5 |- (E.y(ph /\ z = A) -> A.x(A.y(ph -> A e. x) -> z e. x))
34		vex 2863	. . . . . 6 |- z e. _V
35	34	elintab 3938	. . . . 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 203	. . . 4 |- (E.y(ph /\ z = A) -> z e. |^|{x | A.y(ph -> A e. x)})
37	36	abssi 3342	. . 3 |- {z | E.y(ph /\ z = A)} C_ |^|{x | A.y(ph -> A e. x)}
38	24, 37	eqssi 3289	. 2 |- |^|{x | A.y(ph -> A e. x)} = {z | E.y(ph /\ z = A)}
39	38, 4	eqtri 2373	1 |- |^|{x | A.y(ph -> A e. x)} = {x | E.y(ph /\ x = A)}

Syntax hints:   -> wi 4   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  _Vcvv 2860   [.wsbc 3047   C_ wss 3258  |^|cint 3927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-ss 3260  df-int 3928

This theorem is referenced by: (None)