Theorem dfiin2g 4958

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 3068	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵))
2		df-ral 3068	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶))
3		eleq2 2827	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	biimprcd 249	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
5	4	alrimiv 1931	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐵 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
6		eqid 2738	. . . . . . . . . . . 12 ⊢ 𝐵 = 𝐵
7		eqeq1 2742	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐵 → (𝑧 = 𝐵 ↔ 𝐵 = 𝐵))
8	7, 3	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → ((𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝐵 = 𝐵 → 𝑤 ∈ 𝐵)))
9	8	spcgv 3525	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝐶 → (∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧) → (𝐵 = 𝐵 → 𝑤 ∈ 𝐵)))
10	6, 9	mpii 46	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝐶 → (∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧) → 𝑤 ∈ 𝐵))
11	5, 10	impbid2 225	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
12	11	imim2i 16	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
13	12	pm5.74d 272	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
14	13	alimi 1815	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
15		albi 1822	. . . . . . 7 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
16	14, 15	syl 17	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
17	2, 16	sylbi 216	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
18		df-ral 3068	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
19	18	albii 1823	. . . . . . 7 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
20		alcom 2158	. . . . . . 7 ⊢ (∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
21	19, 20	bitr4i 277	. . . . . 6 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
22		r19.23v 3207	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
23		vex 3426	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
24		eqeq1 2742	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
25	24	rexbidv 3225	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
26	23, 25	elab 3602	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
27	26	imbi1i 349	. . . . . . . 8 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
28	22, 27	bitr4i 277	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
29	28	albii 1823	. . . . . 6 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
30		19.21v 1943	. . . . . . 7 ⊢ (∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
31	30	albii 1823	. . . . . 6 ⊢ (∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
32	21, 29, 31	3bitr3ri 301	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
33	17, 32	bitrdi 286	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)))
34	1, 33	syl5bb 282	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)))
35	34	abbidv 2808	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)})
36		df-iin 4924	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵}
37		df-int 4877	. 2 ⊢ ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)}
38	35, 36, 37	3eqtr4g 2804	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2108  {cab 2715  ∀wral 3063  ∃wrex 3064  ∩ cint 4876  ∩ ciin 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-int 4877  df-iin 4924

This theorem is referenced by:  dfiin2  4960  iinexg  5260  dfiin3g  5863  iinfi  9106  mreiincl  17222  iinopn  21959  clsval2  22109  alexsublem  23103