Theorem dfiun2g 4997

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 2142, ax-12 2178. (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 4960	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		elisset 2811	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐶 → ∃𝑧 𝑧 = 𝐵)
3		eleq2 2818	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	pm5.32ri 575	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵))
5	4	simplbi2 500	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
6	5	eximdv 1917	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
7	2, 6	syl5com 31	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
8	7	ralimi 3067	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
9		rexim 3071	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)) → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
10	8, 9	syl 17	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
11		rexcom4 3265	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))
12		r19.42v 3170	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
13	12	exbii 1848	. . . . . . 7 ⊢ (∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
14	11, 13	bitri 275	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
15	10, 14	imbitrdi 251	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
16	3	biimpac 478	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → 𝑤 ∈ 𝐵)
17	16	reximi 3068	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
18	12, 17	sylbir 235	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
19	18	exlimiv 1930	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
20	15, 19	impbid1 225	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
21		vex 3454	. . . . 5 ⊢ 𝑤 ∈ V
22		eleq1w 2812	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
23	22	rexbidv 3158	. . . . 5 ⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵))
24	21, 23	elab 3649	. . . 4 ⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
25		eluni 4877	. . . . 5 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
26		vex 3454	. . . . . . . 8 ⊢ 𝑧 ∈ V
27		eqeq1 2734	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
28	27	rexbidv 3158	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
29	26, 28	elab 3649	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
30	29	anbi2i 623	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
31	30	exbii 1848	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
32	25, 31	bitri 275	. . . 4 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
33	20, 24, 32	3bitr4g 314	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ 𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
34	33	eqrdv 2728	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
35	1, 34	eqtrid 2777	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2708  ∀wral 3045  ∃wrex 3054  ∪ cuni 4874  ∪ ciun 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3452  df-uni 4875  df-iun 4960

This theorem is referenced by:  dfiun2  5000  dfiun3g  5934  abnexg  7735  iunexg  7945  uniqs  8750  ac6num  10439  iunopn  22792  pnrmopn  23237  cncmp  23286  ptcmplem3  23948  iunmbl  25461  voliun  25462  sigaclcuni  34115  sigaclcu2  34117  sigaclci  34129  measvunilem  34209  meascnbl  34216  carsgclctunlem3  34318