Theorem dfbigcup2

Description: Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	dfbigcup2	⊢ Bigcup = ( 𝑥 ∈ V ↦ ∪ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		relbigcup	⊢ Rel Bigcup
2		mptrel	⊢ Rel ( 𝑥 ∈ V ↦ ∪ 𝑥 )
3		eqcom	⊢ ( ∪ 𝑦 = 𝑧 ↔ 𝑧 = ∪ 𝑦 )
4		vex	⊢ 𝑧 ∈ V
5	4	brbigcup	⊢ ( 𝑦 Bigcup 𝑧 ↔ ∪ 𝑦 = 𝑧 )
6		vex	⊢ 𝑦 ∈ V
7		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ V ↔ 𝑦 ∈ V ) )
8		unieq	⊢ ( 𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦 )
9	8	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑡 = ∪ 𝑥 ↔ 𝑡 = ∪ 𝑦 ) )
10	7 9	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ V ∧ 𝑡 = ∪ 𝑥 ) ↔ ( 𝑦 ∈ V ∧ 𝑡 = ∪ 𝑦 ) ) )
11	6	biantrur	⊢ ( 𝑡 = ∪ 𝑦 ↔ ( 𝑦 ∈ V ∧ 𝑡 = ∪ 𝑦 ) )
12	10 11	bitr4di	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ V ∧ 𝑡 = ∪ 𝑥 ) ↔ 𝑡 = ∪ 𝑦 ) )
13		eqeq1	⊢ ( 𝑡 = 𝑧 → ( 𝑡 = ∪ 𝑦 ↔ 𝑧 = ∪ 𝑦 ) )
14		df-mpt	⊢ ( 𝑥 ∈ V ↦ ∪ 𝑥 ) = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑡 = ∪ 𝑥 ) }
15	6 4 12 13 14	brab	⊢ ( 𝑦 ( 𝑥 ∈ V ↦ ∪ 𝑥 ) 𝑧 ↔ 𝑧 = ∪ 𝑦 )
16	3 5 15	3bitr4i	⊢ ( 𝑦 Bigcup 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ∪ 𝑥 ) 𝑧 )
17	1 2 16	eqbrriv	⊢ Bigcup = ( 𝑥 ∈ V ↦ ∪ 𝑥 )