Theorem intab 3957

Description: The intersection of a special case of a class abstraction. y may be free in φ and A, which can be thought of a φ(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 ∈ V
intab.2	⊢ {x ∣ ∃y(φ ∧ x = A)} ∈ V

Assertion

Ref	Expression
intab	⊢ ∩{x ∣ ∀y(φ → A ∈ x)} = {x ∣ ∃y(φ ∧ x = A)}

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

Allowed substitution hints:   φ(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 → ((φ ∧ z = A) ↔ (φ ∧ x = A)))
3	2	exbidv 1626	. . . . . . . 8 ⊢ (z = x → (∃y(φ ∧ z = A) ↔ ∃y(φ ∧ x = A)))
4	3	cbvabv 2473	. . . . . . 7 ⊢ {z ∣ ∃y(φ ∧ z = A)} = {x ∣ ∃y(φ ∧ x = A)}
5		intab.2	. . . . . . 7 ⊢ {x ∣ ∃y(φ ∧ x = A)} ∈ V
6	4, 5	eqeltri 2423	. . . . . 6 ⊢ {z ∣ ∃y(φ ∧ z = A)} ∈ V
7		nfe1 1732	. . . . . . . . 9 ⊢ Ⅎy∃y(φ ∧ z = A)
8	7	nfab 2494	. . . . . . . 8 ⊢ Ⅎy{z ∣ ∃y(φ ∧ z = A)}
9	8	nfeq2 2501	. . . . . . 7 ⊢ Ⅎy x = {z ∣ ∃y(φ ∧ z = A)}
10		eleq2 2414	. . . . . . . 8 ⊢ (x = {z ∣ ∃y(φ ∧ z = A)} → (A ∈ x ↔ A ∈ {z ∣ ∃y(φ ∧ z = A)}))
11	10	imbi2d 307	. . . . . . 7 ⊢ (x = {z ∣ ∃y(φ ∧ z = A)} → ((φ → A ∈ x) ↔ (φ → A ∈ {z ∣ ∃y(φ ∧ z = A)})))
12	9, 11	albid 1772	. . . . . 6 ⊢ (x = {z ∣ ∃y(φ ∧ z = A)} → (∀y(φ → A ∈ x) ↔ ∀y(φ → A ∈ {z ∣ ∃y(φ ∧ z = A)})))
13	6, 12	elab 2986	. . . . 5 ⊢ ({z ∣ ∃y(φ ∧ z = A)} ∈ {x ∣ ∀y(φ → A ∈ x)} ↔ ∀y(φ → A ∈ {z ∣ ∃y(φ ∧ z = A)}))
14		19.8a 1756	. . . . . . . . 9 ⊢ ((φ ∧ z = A) → ∃y(φ ∧ z = A))
15	14	ex 423	. . . . . . . 8 ⊢ (φ → (z = A → ∃y(φ ∧ z = A)))
16	15	alrimiv 1631	. . . . . . 7 ⊢ (φ → ∀z(z = A → ∃y(φ ∧ z = A)))
17		intab.1	. . . . . . . 8 ⊢ A ∈ V
18	17	sbc6 3073	. . . . . . 7 ⊢ ([̣A / z]̣∃y(φ ∧ z = A) ↔ ∀z(z = A → ∃y(φ ∧ z = A)))
19	16, 18	sylibr 203	. . . . . 6 ⊢ (φ → [̣A / z]̣∃y(φ ∧ z = A))
20		df-sbc 3048	. . . . . 6 ⊢ ([̣A / z]̣∃y(φ ∧ z = A) ↔ A ∈ {z ∣ ∃y(φ ∧ z = A)})
21	19, 20	sylib 188	. . . . 5 ⊢ (φ → A ∈ {z ∣ ∃y(φ ∧ z = A)})
22	13, 21	mpgbir 1550	. . . 4 ⊢ {z ∣ ∃y(φ ∧ z = A)} ∈ {x ∣ ∀y(φ → A ∈ x)}
23		intss1 3942	. . . 4 ⊢ ({z ∣ ∃y(φ ∧ z = A)} ∈ {x ∣ ∀y(φ → A ∈ x)} → ∩{x ∣ ∀y(φ → A ∈ x)} ⊆ {z ∣ ∃y(φ ∧ z = A)})
24	22, 23	ax-mp 5	. . 3 ⊢ ∩{x ∣ ∀y(φ → A ∈ x)} ⊆ {z ∣ ∃y(φ ∧ z = A)}
25		19.29r 1597	. . . . . . . 8 ⊢ ((∃y(φ ∧ z = A) ∧ ∀y(φ → A ∈ x)) → ∃y((φ ∧ z = A) ∧ (φ → A ∈ x)))
26		simplr 731	. . . . . . . . . 10 ⊢ (((φ ∧ z = A) ∧ (φ → A ∈ x)) → z = A)
27		pm3.35 570	. . . . . . . . . . 11 ⊢ ((φ ∧ (φ → A ∈ x)) → A ∈ x)
28	27	adantlr 695	. . . . . . . . . 10 ⊢ (((φ ∧ z = A) ∧ (φ → A ∈ x)) → A ∈ x)
29	26, 28	eqeltrd 2427	. . . . . . . . 9 ⊢ (((φ ∧ z = A) ∧ (φ → A ∈ x)) → z ∈ x)
30	29	exlimiv 1634	. . . . . . . 8 ⊢ (∃y((φ ∧ z = A) ∧ (φ → A ∈ x)) → z ∈ x)
31	25, 30	syl 15	. . . . . . 7 ⊢ ((∃y(φ ∧ z = A) ∧ ∀y(φ → A ∈ x)) → z ∈ x)
32	31	ex 423	. . . . . 6 ⊢ (∃y(φ ∧ z = A) → (∀y(φ → A ∈ x) → z ∈ x))
33	32	alrimiv 1631	. . . . 5 ⊢ (∃y(φ ∧ z = A) → ∀x(∀y(φ → A ∈ x) → z ∈ x))
34		vex 2863	. . . . . 6 ⊢ z ∈ V
35	34	elintab 3938	. . . . 5 ⊢ (z ∈ ∩{x ∣ ∀y(φ → A ∈ x)} ↔ ∀x(∀y(φ → A ∈ x) → z ∈ x))
36	33, 35	sylibr 203	. . . 4 ⊢ (∃y(φ ∧ z = A) → z ∈ ∩{x ∣ ∀y(φ → A ∈ x)})
37	36	abssi 3342	. . 3 ⊢ {z ∣ ∃y(φ ∧ z = A)} ⊆ ∩{x ∣ ∀y(φ → A ∈ x)}
38	24, 37	eqssi 3289	. 2 ⊢ ∩{x ∣ ∀y(φ → A ∈ x)} = {z ∣ ∃y(φ ∧ z = A)}
39	38, 4	eqtri 2373	1 ⊢ ∩{x ∣ ∀y(φ → A ∈ x)} = {x ∣ ∃y(φ ∧ x = A)}

This proof depends on syntax axioms:   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  Vcvv 2860  [̣wsbc 3047   ⊆ wss 3258  ∩cint 3927

This proof depends on 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 proof 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 used by: (None)