Theorem dfiun2g 4987

Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) Avoid ax-10 2177, ax-12 2212. (Revised by SN, 11-Dec-2024.)

Assertion

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

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

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

Proof of Theorem dfiun2g

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

Step	Hyp	Ref	Expression
1		df-iun 4952	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		elisset 2842	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐶 → ∃𝑧 𝑧 = 𝐵)
3		eleq2 2849	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	pm5.32ri 586	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵))
5	4	simplbi2 506	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
6	5	eximdv 1949	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
7	2, 6	syl5com 32	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
8	7	ralimi 3099	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
9		rexim 3103	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)) → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
10	8, 9	syl 18	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
11		rexcom4 3289	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))
12		r19.42v 3194	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
13	12	exbii 1880	. . . . . . 7 ⊢ (∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
14	11, 13	bitri 278	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
15	10, 14	imbitrdi 254	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
16	3	biimpac 484	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → 𝑤 ∈ 𝐵)
17	16	reximi 3100	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
18	12, 17	sylbir 238	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
19	18	exlimiv 1962	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
20	15, 19	impbid1 228	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
21		vex 3454	. . . . 5 ⊢ 𝑤 ∈ V
22		eleq1w 2843	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
23	22	rexbidv 3186	. . . . 5 ⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵))
24	21, 23	elab 3632	. . . 4 ⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
25		eluni 4869	. . . . 5 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
26		vex 3454	. . . . . . . 8 ⊢ 𝑧 ∈ V
27		eqeq1 2764	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
28	27	rexbidv 3186	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
29	26, 28	elab 3632	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
30	29	anbi2i 635	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
31	30	exbii 1880	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
32	25, 31	bitri 278	. . . 4 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
33	20, 24, 32	3bitr4g 317	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ 𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
34	33	eqrdv 2758	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
35	1, 34	eqtrid 2807	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  ∪ cuni 4866  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-11 2193  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-uni 4867  df-iun 4952

This theorem is used by:  dfiun2  4989  dfiun3g  5949  abnexg  7770  iunexg  7975  uniqs  8794  ac6num  10557  iunopn  23216  pnrmopn  23661  cncmp  23710  ptcmplem3  24373  iunmbl  25874  voliun  25875  sigaclcuni  34750  sigaclcu2  34752  sigaclci  34764  measvunilem  34845  meascnbl  34852  carsgclctunlem3  34952