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\in \mathrm{V}$$
	intab.2	$$⊢\left\{x|\exists y\left(\phi \wedge x=A\right)\right\}\in \mathrm{V}$$
Assertion	intab	$$⊢\bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}=\left\{x|\exists y\left(\phi \wedge x=A\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		intab.1	$$⊢A\in \mathrm{V}$$
2		intab.2	$$⊢\left\{x|\exists y\left(\phi \wedge x=A\right)\right\}\in \mathrm{V}$$
3		eqeq1	$$⊢z=x\to \left(z=A\leftrightarrow x=A\right)$$
4	3	anbi2d	$$⊢z=x\to \left(\left(\phi \wedge z=A\right)\leftrightarrow \left(\phi \wedge x=A\right)\right)$$
5	4	exbidv	$$⊢z=x\to \left(\exists y\left(\phi \wedge z=A\right)\leftrightarrow \exists y\left(\phi \wedge x=A\right)\right)$$
6	5	cbvabv	$$⊢\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}=\left\{x|\exists y\left(\phi \wedge x=A\right)\right\}$$
7	6 2	eqeltri	$$⊢\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\in \mathrm{V}$$
8		nfe1	$$⊢Ⅎy\exists y\left(\phi \wedge z=A\right)$$
9	8	nfab	$$⊢\underset{\_}{Ⅎ}y\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
10	9	nfeq2	$$⊢Ⅎyx=\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
11		eleq2	$$⊢x=\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\to \left(A\in x\leftrightarrow A\in \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\right)$$
12	11	imbi2d	$$⊢x=\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\to \left(\left(\phi \to A\in x\right)\leftrightarrow \left(\phi \to A\in \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\right)\right)$$
13	10 12	albid	$$⊢x=\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\to \left(\forall y\left(\phi \to A\in x\right)\leftrightarrow \forall y\left(\phi \to A\in \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\right)\right)$$
14	7 13	elab	$$⊢\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\in \left\{x|\forall y\left(\phi \to A\in x\right)\right\}\leftrightarrow \forall y\left(\phi \to A\in \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\right)$$
15		19.8a	$$⊢\left(\phi \wedge z=A\right)\to \exists y\left(\phi \wedge z=A\right)$$
16	15	ex	$$⊢\phi \to \left(z=A\to \exists y\left(\phi \wedge z=A\right)\right)$$
17	16	alrimiv	$$⊢\phi \to \forall z\left(z=A\to \exists y\left(\phi \wedge z=A\right)\right)$$
18	1	sbc6	$$⊢\underset{\dot{}}{[}A/z\underset{\dot{}}{]}\exists y\left(\phi \wedge z=A\right)\leftrightarrow \forall z\left(z=A\to \exists y\left(\phi \wedge z=A\right)\right)$$
19	17 18	sylibr	$$⊢\phi \to \underset{\dot{}}{[}A/z\underset{\dot{}}{]}\exists y\left(\phi \wedge z=A\right)$$
20		df-sbc	$$⊢\underset{\dot{}}{[}A/z\underset{\dot{}}{]}\exists y\left(\phi \wedge z=A\right)\leftrightarrow A\in \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
21	19 20	sylib	$$⊢\phi \to A\in \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
22	14 21	mpgbir	$$⊢\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\in \left\{x|\forall y\left(\phi \to A\in x\right)\right\}$$
23		intss1	$$⊢\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\in \left\{x|\forall y\left(\phi \to A\in x\right)\right\}\to \bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}\subseteq \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
24	22 23	ax-mp	$$⊢\bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}\subseteq \left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
25		19.29r	$$⊢\left(\exists y\left(\phi \wedge z=A\right)\wedge \forall y\left(\phi \to A\in x\right)\right)\to \exists y\left(\left(\phi \wedge z=A\right)\wedge \left(\phi \to A\in x\right)\right)$$
26		simplr	$$⊢\left(\left(\phi \wedge z=A\right)\wedge \left(\phi \to A\in x\right)\right)\to z=A$$
27		pm3.35	$$⊢\left(\phi \wedge \left(\phi \to A\in x\right)\right)\to A\in x$$
28	27	adantlr	$$⊢\left(\left(\phi \wedge z=A\right)\wedge \left(\phi \to A\in x\right)\right)\to A\in x$$
29	26 28	eqeltrd	$$⊢\left(\left(\phi \wedge z=A\right)\wedge \left(\phi \to A\in x\right)\right)\to z\in x$$
30	29	exlimiv	$$⊢\exists y\left(\left(\phi \wedge z=A\right)\wedge \left(\phi \to A\in x\right)\right)\to z\in x$$
31	25 30	syl	$$⊢\left(\exists y\left(\phi \wedge z=A\right)\wedge \forall y\left(\phi \to A\in x\right)\right)\to z\in x$$
32	31	ex	$$⊢\exists y\left(\phi \wedge z=A\right)\to \left(\forall y\left(\phi \to A\in x\right)\to z\in x\right)$$
33	32	alrimiv	$$⊢\exists y\left(\phi \wedge z=A\right)\to \forall x\left(\forall y\left(\phi \to A\in x\right)\to z\in x\right)$$
34		vex	$$⊢z\in \mathrm{V}$$
35	34	elintab	$$⊢z\in \bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}\leftrightarrow \forall x\left(\forall y\left(\phi \to A\in x\right)\to z\in x\right)$$
36	33 35	sylibr	$$⊢\exists y\left(\phi \wedge z=A\right)\to z\in \bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}$$
37	36	abssi	$$⊢\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}\subseteq \bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}$$
38	24 37	eqssi	$$⊢\bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}=\left\{z|\exists y\left(\phi \wedge z=A\right)\right\}$$
39	38 6	eqtri	$$⊢\bigcap \left\{x|\forall y\left(\phi \to A\in x\right)\right\}=\left\{x|\exists y\left(\phi \wedge x=A\right)\right\}$$