Theorem dfiun2g

Description: Alternate definition of indexed union when B 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 , ax-12 . (Revised by SN, 11-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 }
2		elisset	⊢ ( 𝐵 ∈ 𝐶 → ∃ 𝑧 𝑧 = 𝐵 )
3		eleq2	⊢ ( 𝑧 = 𝐵 → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵 ) )
4	3	pm5.32ri	⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵 ) )
5	4	simplbi2	⊢ ( 𝑤 ∈ 𝐵 → ( 𝑧 = 𝐵 → ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
6	5	eximdv	⊢ ( 𝑤 ∈ 𝐵 → ( ∃ 𝑧 𝑧 = 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
7	2 6	syl5com	⊢ ( 𝐵 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
8	7	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∀ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
9		rexim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
10	8 9	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
11		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) )
12		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
13	12	exbii	⊢ ( ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
14	11 13	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
15	10 14	imbitrdi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) ) )
16	3	biimpac	⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) → 𝑤 ∈ 𝐵 )
17	16	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
18	12 17	sylbir	⊢ ( ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
19	18	exlimiv	⊢ ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
20	15 19	impbid1	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) ) )
21		vex	⊢ 𝑤 ∈ V
22		eleq1w	⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
23	22	rexbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ) )
24	21 23	elab	⊢ ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
25		eluni	⊢ ( 𝑤 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
26		vex	⊢ 𝑧 ∈ V
27		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑧 = 𝐵 ) )
28	27	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
29	26 28	elab	⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
30	29	anbi2i	⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
31	30	exbii	⊢ ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
32	25 31	bitri	⊢ ( 𝑤 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
33	20 24 32	3bitr4g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ 𝑤 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
34	33	eqrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
35	1 34	eqtrid	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )