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 2147, ax-12 2185. (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 4950	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		elisset 2819	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐶 → ∃𝑧 𝑧 = 𝐵)
3		eleq2 2826	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	pm5.32ri 575	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵))
5	4	simplbi2 500	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
6	5	eximdv 1919	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
7	2, 6	syl5com 31	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
8	7	ralimi 3075	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
9		rexim 3079	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)) → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
10	8, 9	syl 17	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
11		rexcom4 3265	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))
12		r19.42v 3170	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
13	12	exbii 1850	. . . . . . 7 ⊢ (∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
14	11, 13	bitri 275	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
15	10, 14	imbitrdi 251	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
16	3	biimpac 478	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → 𝑤 ∈ 𝐵)
17	16	reximi 3076	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
18	12, 17	sylbir 235	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
19	18	exlimiv 1932	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
20	15, 19	impbid1 225	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
21		vex 3446	. . . . 5 ⊢ 𝑤 ∈ V
22		eleq1w 2820	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
23	22	rexbidv 3162	. . . . 5 ⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵))
24	21, 23	elab 3636	. . . 4 ⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
25		eluni 4868	. . . . 5 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
26		vex 3446	. . . . . . . 8 ⊢ 𝑧 ∈ V
27		eqeq1 2741	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
28	27	rexbidv 3162	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
29	26, 28	elab 3636	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
30	29	anbi2i 624	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
31	30	exbii 1850	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
32	25, 31	bitri 275	. . . 4 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
33	20, 24, 32	3bitr4g 314	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ 𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
34	33	eqrdv 2735	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
35	1, 34	eqtrid 2784	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  ∪ cuni 4865  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-uni 4866  df-iun 4950

This theorem is referenced by:  dfiun2  4989  dfiun3g  5927  abnexg  7713  iunexg  7919  uniqs  8724  ac6num  10403  iunopn  22859  pnrmopn  23304  cncmp  23353  ptcmplem3  24015  iunmbl  25527  voliun  25528  sigaclcuni  34302  sigaclcu2  34304  sigaclci  34316  measvunilem  34396  meascnbl  34403  carsgclctunlem3  34504