Theorem dfiin2g 3690

Description: Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)

Assertion

Ref	Expression
dfiin2g	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem dfiin2g

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ral 2311	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵))
2		df-ral 2311	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶))
3		eleq2 2101	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	biimprcd 149	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
5	4	alrimiv 1754	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐵 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
6		eqid 2040	. . . . . . . . . . . 12 ⊢ 𝐵 = 𝐵
7		eqeq1 2046	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐵 → (𝑧 = 𝐵 ↔ 𝐵 = 𝐵))
8	7, 3	imbi12d 223	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → ((𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝐵 = 𝐵 → 𝑤 ∈ 𝐵)))
9	8	spcgv 2640	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝐶 → (∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧) → (𝐵 = 𝐵 → 𝑤 ∈ 𝐵)))
10	6, 9	mpii 39	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐶 → (∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧) → 𝑤 ∈ 𝐵))
11	5, 10	impbid2 131	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
12	11	imim2i 12	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
13	12	pm5.74d 171	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
14	13	alimi 1344	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
15		albi 1357	. . . . . . 7 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
16	14, 15	syl 14	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
17	2, 16	sylbi 114	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
18		df-ral 2311	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
19	18	albii 1359	. . . . . . 7 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
20		alcom 1367	. . . . . . 7 ⊢ (∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
21	19, 20	bitr4i 176	. . . . . 6 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
22		r19.23v 2425	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
23		vex 2560	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
24		eqeq1 2046	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
25	24	rexbidv 2327	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
26	23, 25	elab 2687	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
27	26	imbi1i 227	. . . . . . . 8 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
28	22, 27	bitr4i 176	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
29	28	albii 1359	. . . . . 6 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
30		19.21v 1753	. . . . . . 7 ⊢ (∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
31	30	albii 1359	. . . . . 6 ⊢ (∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
32	21, 29, 31	3bitr3ri 200	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
33	17, 32	syl6bb 185	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)))
34	1, 33	syl5bb 181	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)))
35	34	abbidv 2155	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)})
36		df-iin 3660	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵}
37		df-int 3616	. 2 ⊢ ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)}
38	35, 36, 37	3eqtr4g 2097	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393  {cab 2026  ∀wral 2306  ∃wrex 2307  ∩ cint 3615  ∩ ciin 3658

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-int 3616  df-iin 3660

This theorem is referenced by:  dfiin2  3692  iinexgm  3908  dfiin3g  4590  fniinfv  5231