Theorem dfiun2g 4705

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.)

Assertion

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

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

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

Proof of Theorem dfiun2g

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfra1 3080	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶
2		rsp 3068	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶))
3		clel3g 3481	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐶 → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)))
4	2, 3	syl6 35	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑥 ∈ 𝐴 → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))))
5	4	imp 444	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)))
6	1, 5	rexbida 3186	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)))
7		rexcom4 3366	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦(𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))
8	6, 7	syl6bb 276	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦)))
9		r19.41v 3228	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))
10	9	exbii 1923	. . . . 5 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦))
11		exancom 1936	. . . . 5 ⊢ (∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵))
12	10, 11	bitri 264	. . . 4 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝑦) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵))
13	8, 12	syl6bb 276	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)))
14		eliun 4677	. . 3 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)
15		eluniab 4600	. . 3 ⊢ (𝑧 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵))
16	13, 14, 15	3bitr4g 303	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑧 ∈ ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}))
17	16	eqrdv 2759	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632  ∃wex 1853   ∈ wcel 2140  {cab 2747  ∀wral 3051  ∃wrex 3052  ∪ cuni 4589  ∪ ciun 4673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-v 3343  df-uni 4590  df-iun 4675

This theorem is referenced by:  dfiun2  4707  dfiun3g  5534  abnexg  7131  iunexg  7310  uniqs  7977  ac6num  9514  iunopn  20926  pnrmopn  21370  cncmp  21418  ptcmplem3  22080  iunmbl  23542  voliun  23543  sigaclcuni  30512  sigaclcu2  30514  sigaclci  30526  measvunilem  30606  meascnbl  30613  carsgclctunlem3  30713  uniqsALTV  34444