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	⊢ 𝐴 ∈ V
	intab.2	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) } ∈ V
Assertion	intab	⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) }

Proof

Step	Hyp	Ref	Expression
1		intab.1	⊢ 𝐴 ∈ V
2		intab.2	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) } ∈ V
3		eqeq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝐴 ↔ 𝑥 = 𝐴 ) )
4	3	anbi2d	⊢ ( 𝑧 = 𝑥 → ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
5	4	exbidv	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
6	5	cbvabv	⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) }
7	6 2	eqeltri	⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ V
8		nfe1	⊢ Ⅎ 𝑦 ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 )
9	8	nfab	⊢ Ⅎ 𝑦 { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
10	9	nfeq2	⊢ Ⅎ 𝑦 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
11		eleq2	⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) )
12	11	imbi2d	⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } → ( ( 𝜑 → 𝐴 ∈ 𝑥 ) ↔ ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) ) )
13	10 12	albid	⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } → ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) ) )
14	7 13	elab	⊢ ( { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ↔ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) )
15		19.8a	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐴 ) → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) )
16	15	ex	⊢ ( 𝜑 → ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ) )
17	16	alrimiv	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ) )
18	1	sbc6	⊢ ( [ 𝐴 / 𝑧 ] ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ ∀ 𝑧 ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ) )
19	17 18	sylibr	⊢ ( 𝜑 → [ 𝐴 / 𝑧 ] ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) )
20		df-sbc	⊢ ( [ 𝐴 / 𝑧 ] ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } )
21	19 20	sylib	⊢ ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } )
22	14 21	mpgbir	⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) }
23		intss1	⊢ ( { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } → ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ⊆ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } )
24	22 23	ax-mp	⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ⊆ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
25		19.29r	⊢ ( ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → ∃ 𝑦 ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
26		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 = 𝐴 )
27		pm3.35	⊢ ( ( 𝜑 ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝐴 ∈ 𝑥 )
28	27	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝐴 ∈ 𝑥 )
29	26 28	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
30	29	exlimiv	⊢ ( ∃ 𝑦 ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
31	25 30	syl	⊢ ( ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
32	31	ex	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) → ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
33	32	alrimiv	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) → ∀ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
34		vex	⊢ 𝑧 ∈ V
35	34	elintab	⊢ ( 𝑧 ∈ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
36	33 35	sylibr	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) → 𝑧 ∈ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } )
37	36	abssi	⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ⊆ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) }
38	24 37	eqssi	⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
39	38 6	eqtri	⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) }