Theorem dfiin2g 4962

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 3069	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵))
2		df-ral 3069	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶))
3		eleq2 2827	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	biimprcd 249	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
5	4	alrimiv 1930	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐵 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
6		eqid 2738	. . . . . . . . . . . 12 ⊢ 𝐵 = 𝐵
7		eqeq1 2742	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐵 → (𝑧 = 𝐵 ↔ 𝐵 = 𝐵))
8	7, 3	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → ((𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝐵 = 𝐵 → 𝑤 ∈ 𝐵)))
9	8	spcgv 3535	. . . . . . . . . . . 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 1814	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → ∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
15		albi 1821	. . . . . . 7 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
16	14, 15	syl 17	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
17	2, 16	sylbi 216	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧))))
18		df-ral 3069	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
19	18	albii 1822	. . . . . . 7 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
20		alcom 2156	. . . . . . 7 ⊢ (∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧∀𝑥(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
21	19, 20	bitr4i 277	. . . . . 6 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
22		r19.23v 3208	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
23		vex 3436	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
24		eqeq1 2742	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
25	24	rexbidv 3226	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
26	23, 25	elab 3609	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
27	26	imbi1i 350	. . . . . . . 8 ⊢ ((𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧) ↔ (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧))
28	22, 27	bitr4i 277	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
29	28	albii 1822	. . . . . 6 ⊢ (∀𝑧∀𝑥 ∈ 𝐴 (𝑧 = 𝐵 → 𝑤 ∈ 𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
30		19.21v 1942	. . . . . . 7 ⊢ (∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
31	30	albii 1822	. . . . . 6 ⊢ (∀𝑥∀𝑧(𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)))
32	21, 29, 31	3bitr3ri 302	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑧(𝑧 = 𝐵 → 𝑤 ∈ 𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧))
33	17, 32	bitrdi 287	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)))
34	1, 33	bitrid 282	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)))
35	34	abbidv 2807	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)})
36		df-iin 4927	. 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑤 ∣ ∀𝑥 ∈ 𝐴 𝑤 ∈ 𝐵}
37		df-int 4880	. 2 ⊢ ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} → 𝑤 ∈ 𝑧)}
38	35, 36, 37	3eqtr4g 2803	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2106  {cab 2715  ∀wral 3064  ∃wrex 3065  ∩ cint 4879  ∩ ciin 4925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-int 4880  df-iin 4927

This theorem is referenced by:  dfiin2  4964  iinexg  5265  dfiin3g  5874  iinfi  9176  mreiincl  17305  iinopn  22051  clsval2  22201  alexsublem  23195