Theorem dfiun2g 4992

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 2178, ax-12 2215. (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 4956	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		elisset 2844	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝐶 → ∃𝑧 𝑧 = 𝐵)
3		eleq2 2851	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵))
4	3	pm5.32ri 586	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵))
5	4	simplbi2 506	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐵 → (𝑧 = 𝐵 → (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
6	5	eximdv 1950	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐵 → (∃𝑧 𝑧 = 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
7	2, 6	syl5com 32	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐶 → (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
8	7	ralimi 3101	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
9		rexim 3105	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)) → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
10	8, 9	syl 18	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵)))
11		rexcom4 3291	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵))
12		r19.42v 3196	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
13	12	exbii 1881	. . . . . . 7 ⊢ (∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
14	11, 13	bitri 278	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
15	10, 14	imbitrdi 254	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
16	3	biimpac 484	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → 𝑤 ∈ 𝐵)
17	16	reximi 3102	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
18	12, 17	sylbir 238	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
19	18	exlimiv 1963	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
20	15, 19	impbid1 228	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)))
21		vex 3457	. . . . 5 ⊢ 𝑤 ∈ V
22		eleq1w 2845	. . . . . 6 ⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵))
23	22	rexbidv 3188	. . . . 5 ⊢ (𝑧 = 𝑤 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵))
24	21, 23	elab 3636	. . . 4 ⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ 𝐵)
25		eluni 4873	. . . . 5 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
26		vex 3457	. . . . . . . 8 ⊢ 𝑧 ∈ V
27		eqeq1 2766	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = 𝐵 ↔ 𝑧 = 𝐵))
28	27	rexbidv 3188	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
29	26, 28	elab 3636	. . . . . . 7 ⊢ (𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)
30	29	anbi2i 635	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
31	30	exbii 1881	. . . . 5 ⊢ (∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
32	25, 31	bitri 278	. . . 4 ⊢ (𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵))
33	20, 24, 32	3bitr4g 317	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑤 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} ↔ 𝑤 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
34	33	eqrdv 2760	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
35	1, 34	eqtrid 2809	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2740  ∀wral 3078  ∃wrex 3088  ∪ cuni 4870  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-v 3455  df-uni 4871  df-iun 4956

This theorem is used by:  dfiun2  4994  dfiun3g  5956  abnexg  7758  iunexg  7963  uniqs  8776  ac6num  10484  iunopn  23122  pnrmopn  23567  cncmp  23616  ptcmplem3  24279  iunmbl  25780  voliun  25781  sigaclcuni  34613  sigaclcu2  34615  sigaclci  34627  measvunilem  34708  meascnbl  34715  carsgclctunlem3  34816