Metamath Proof Explorer

Theorem dfbigcup2

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

Ref Expression
Assertion dfbigcup2 ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 = x ∈ V ⟼ ⋃ x

Proof

Step Hyp Ref Expression
1 relbigcup ⊢ Rel ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉
2 mptrel ⊢ Rel ⁡ x ∈ V ⟼ ⋃ x
3 eqcom ⊢ ⋃ y = z ↔ z = ⋃ y
4 vex ⊢ z ∈ V
5 4 brbigcup ⊢ y 𝖡𝗂𝗀𝖼𝗎𝗉 z ↔ ⋃ y = z
6 vex ⊢ y ∈ V
7 eleq1w ⊢ x = y → x ∈ V ↔ y ∈ V
8 unieq ⊢ x = y → ⋃ x = ⋃ y
9 8 eqeq2d ⊢ x = y → t = ⋃ x ↔ t = ⋃ y
10 7 9 anbi12d ⊢ x = y → x ∈ V ∧ t = ⋃ x ↔ y ∈ V ∧ t = ⋃ y
11 6 biantrur ⊢ t = ⋃ y ↔ y ∈ V ∧ t = ⋃ y
12 10 11 bitr4di ⊢ x = y → x ∈ V ∧ t = ⋃ x ↔ t = ⋃ y
13 eqeq1 ⊢ t = z → t = ⋃ y ↔ z = ⋃ y
14 df-mpt ⊢ x ∈ V ⟼ ⋃ x = x t | x ∈ V ∧ t = ⋃ x
15 6 4 12 13 14 brab ⊢ y x ∈ V ⟼ ⋃ x z ↔ z = ⋃ y
16 3 5 15 3bitr4i ⊢ y 𝖡𝗂𝗀𝖼𝗎𝗉 z ↔ y x ∈ V ⟼ ⋃ x z
17 1 2 16 eqbrriv ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 = x ∈ V ⟼ ⋃ x