Theorem intab 2556

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 3866 or abexssex 3867 can be used to satisfy the second hypothesis.

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

Proof of Theorem intab

Step	Hyp	Ref	Expression
1		eqeq1 1479	. . . . . . . . . . 11 ⊢ (z = x → (z = A ↔ x = A))
2	1	anbi2d 615	. . . . . . . . . 10 ⊢ (z = x → ((φ ⋀ z = A) ↔ (φ ⋀ x = A)))
3	2	exbidv 1278	. . . . . . . . 9 ⊢ (z = x → (∃y(φ ⋀ z = A) ↔ ∃y(φ ⋀ x = A)))
4	3	cbvabv 1906	. . . . . . . 8 ⊢ {z∣∃y(φ ⋀ z = A)} = {x∣∃y(φ ⋀ x = A)}
5		intab.2	. . . . . . . 8 ⊢ {x∣∃y(φ ⋀ x = A)} ∈ V
6	4, 5	eqeltr 1542	. . . . . . 7 ⊢ {z∣∃y(φ ⋀ z = A)} ∈ V
7		hbe1 1015	. . . . . . . . . 10 ⊢ (∃y(φ ⋀ z = A) → ∀y∃y(φ ⋀ z = A))
8	7	hbab 1466	. . . . . . . . 9 ⊢ (x ∈ {z∣∃y(φ ⋀ z = A)} → ∀y x ∈ {z∣∃y(φ ⋀ z = A)})
9	8	hbeleq 1565	. . . . . . . 8 ⊢ (x = {z∣∃y(φ ⋀ z = A)} → ∀y x = {z∣∃y(φ ⋀ z = A)})
10		eleq2 1533	. . . . . . . . 9 ⊢ (x = {z∣∃y(φ ⋀ z = A)} → (A ∈ x ↔ A ∈ {z∣∃y(φ ⋀ z = A)}))
11	10	imbi2d 611	. . . . . . . 8 ⊢ (x = {z∣∃y(φ ⋀ z = A)} → ((φ → A ∈ x) ↔ (φ → A ∈ {z∣∃y(φ ⋀ z = A)})))
12	9, 11	albid 1103	. . . . . . 7 ⊢ (x = {z∣∃y(φ ⋀ z = A)} → (∀y(φ → A ∈ x) ↔ ∀y(φ → A ∈ {z∣∃y(φ ⋀ z = A)})))
13	6, 12	sbcie 1959	. . . . . 6 ⊢ ([{z∣∃y(φ ⋀ z = A)} / x]∀y(φ → A ∈ x) ↔ ∀y(φ → A ∈ {z∣∃y(φ ⋀ z = A)}))
14		intab.1	. . . . . . . . . . . 12 ⊢ A ∈ V
15		ax-17 970	. . . . . . . . . . . . 13 ⊢ (φ → ∀zφ)
16	15	sbcgf 1983	. . . . . . . . . . . 12 ⊢ (A ∈ V → ([A / z]φ ↔ φ))
17	14, 16	ax-mp 7	. . . . . . . . . . 11 ⊢ ([A / z]φ ↔ φ)
18	17	biimpr 152	. . . . . . . . . 10 ⊢ (φ → [A / z]φ)
19		csbvarg 2018	. . . . . . . . . . . 12 ⊢ (A ∈ V → [A / z]z = A)
20	14, 19	ax-mp 7	. . . . . . . . . . 11 ⊢ [A / z]z = A
21		sbceq1dig 2011	. . . . . . . . . . . 12 ⊢ (A ∈ V → ([A / z]z = A ↔ [A / z]z = A))
22	14, 21	ax-mp 7	. . . . . . . . . . 11 ⊢ ([A / z]z = A ↔ [A / z]z = A)
23	20, 22	mpbir 190	. . . . . . . . . 10 ⊢ [A / z]z = A
24	18, 23	jctir 293	. . . . . . . . 9 ⊢ (φ → ([A / z]φ ⋀ [A / z]z = A))
25		sbcang 1968	. . . . . . . . . 10 ⊢ (A ∈ V → ([A / z](φ ⋀ z = A) ↔ ([A / z]φ ⋀ [A / z]z = A)))
26	14, 25	ax-mp 7	. . . . . . . . 9 ⊢ ([A / z](φ ⋀ z = A) ↔ ([A / z]φ ⋀ [A / z]z = A))
27	24, 26	sylibr 200	. . . . . . . 8 ⊢ (φ → [A / z](φ ⋀ z = A))
28		19.8a 1028	. . . . . . . . . . 11 ⊢ ((φ ⋀ z = A) → ∃y(φ ⋀ z = A))
29	28	ax-gen 962	. . . . . . . . . 10 ⊢ ∀z((φ ⋀ z = A) → ∃y(φ ⋀ z = A))
30		a4sbc 1942	. . . . . . . . . 10 ⊢ (A ∈ V → (∀z((φ ⋀ z = A) → ∃y(φ ⋀ z = A)) → [A / z]((φ ⋀ z = A) → ∃y(φ ⋀ z = A))))
31	14, 29, 30	mp2 43	. . . . . . . . 9 ⊢ [A / z]((φ ⋀ z = A) → ∃y(φ ⋀ z = A))
32		sbcimg 1967	. . . . . . . . . 10 ⊢ (A ∈ V → ([A / z]((φ ⋀ z = A) → ∃y(φ ⋀ z = A)) ↔ ([A / z](φ ⋀ z = A) → [A / z]∃y(φ ⋀ z = A))))
33	14, 32	ax-mp 7	. . . . . . . . 9 ⊢ ([A / z]((φ ⋀ z = A) → ∃y(φ ⋀ z = A)) ↔ ([A / z](φ ⋀ z = A) → [A / z]∃y(φ ⋀ z = A)))
34	31, 33	mpbi 189	. . . . . . . 8 ⊢ ([A / z](φ ⋀ z = A) → [A / z]∃y(φ ⋀ z = A))
35	27, 34	syl 10	. . . . . . 7 ⊢ (φ → [A / z]∃y(φ ⋀ z = A))
36	14	elabs 1963	. . . . . . 7 ⊢ (A ∈ {z∣∃y(φ ⋀ z = A)} ↔ [A / z]∃y(φ ⋀ z = A))
37	35, 36	sylibr 200	. . . . . 6 ⊢ (φ → A ∈ {z∣∃y(φ ⋀ z = A)})
38	13, 37	mpgbir 987	. . . . 5 ⊢ [{z∣∃y(φ ⋀ z = A)} / x]∀y(φ → A ∈ x)
39	6	elabs 1963	. . . . 5 ⊢ ({z∣∃y(φ ⋀ z = A)} ∈ {x∣∀y(φ → A ∈ x)} ↔ [{z∣∃y(φ ⋀ z = A)} / x]∀y(φ → A ∈ x))
40	38, 39	mpbir 190	. . . 4 ⊢ {z∣∃y(φ ⋀ z = A)} ∈ {x∣∀y(φ → A ∈ x)}
41		intss1 2544	. . . 4 ⊢ ({z∣∃y(φ ⋀ z = A)} ∈ {x∣∀y(φ → A ∈ x)} → ∩{x∣∀y(φ → A ∈ x)} ⊆ {z∣∃y(φ ⋀ z = A)})
42	40, 41	ax-mp 7	. . 3 ⊢ ∩{x∣∀y(φ → A ∈ x)} ⊆ {z∣∃y(φ ⋀ z = A)}
43		hba1 1002	. . . . . . 7 ⊢ (∀y(φ → A ∈ x) → ∀y∀y(φ → A ∈ x))
44	43	hbab 1466	. . . . . 6 ⊢ (z ∈ {x∣∀y(φ → A ∈ x)} → ∀y z ∈ {x∣∀y(φ → A ∈ x)})
45	44	hbint 2539	. . . . 5 ⊢ (z ∈ ∩{x∣∀y(φ → A ∈ x)} → ∀y z ∈ ∩{x∣∀y(φ → A ∈ x)})
46		ax-4 972	. . . . . . . . . 10 ⊢ (∀y(φ → A ∈ x) → (φ → A ∈ x))
47	46	com12 11	. . . . . . . . 9 ⊢ (φ → (∀y(φ → A ∈ x) → A ∈ x))
48	47	adantr 389	. . . . . . . 8 ⊢ ((φ ⋀ z = A) → (∀y(φ → A ∈ x) → A ∈ x))
49		eleq1 1532	. . . . . . . . 9 ⊢ (z = A → (z ∈ x ↔ A ∈ x))
50	49	adantl 388	. . . . . . . 8 ⊢ ((φ ⋀ z = A) → (z ∈ x ↔ A ∈ x))
51	48, 50	sylibrd 204	. . . . . . 7 ⊢ ((φ ⋀ z = A) → (∀y(φ → A ∈ x) → z ∈ x))
52	51	19.21aiv 1285	. . . . . 6 ⊢ ((φ ⋀ z = A) → ∀x(∀y(φ → A ∈ x) → z ∈ x))
53		visset 1810	. . . . . . 7 ⊢ z ∈ V
54	53	elintab 2540	. . . . . 6 ⊢ (z ∈ ∩{x∣∀y(φ → A ∈ x)} ↔ ∀x(∀y(φ → A ∈ x) → z ∈ x))
55	52, 54	sylibr 200	. . . . 5 ⊢ ((φ ⋀ z = A) → z ∈ ∩{x∣∀y(φ → A ∈ x)})
56	45, 55	19.23ai 1063	. . . 4 ⊢ (∃y(φ ⋀ z = A) → z ∈ ∩{x∣∀y(φ → A ∈ x)})
57	56	abssi 2119	. . 3 ⊢ {z∣∃y(φ ⋀ z = A)} ⊆ ∩{x∣∀y(φ → A ∈ x)}
58	42, 57	eqssi 2075	. 2 ⊢ ∩{x∣∀y(φ → A ∈ x)} = {z∣∃y(φ ⋀ z = A)}
59	58, 4	eqtr 1493	1 ⊢ ∩{x∣∀y(φ → A ∈ x)} = {x∣∃y(φ ⋀ x = A)}

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  ∃wex 979  [wsbc 1169  {cab 1462  Vcvv 1808  [csb 1998   ⊆ wss 2044  ∩cint 2529

This theorem is referenced by:  abfii2 4545

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-rab 1650  df-v 1809  df-sbc 1939  df-csb 1999  df-in 2048  df-ss 2050  df-int 2530

Copyright terms: Public domain