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=xt|x∈V∧t=⋃x
15 6 4 12 13 14 brab ⊒yx∈VβŸΌβ‹ƒxz↔z=⋃y
16 3 5 15 3bitr4i ⊒yπ–‘π—‚π—€π–Όπ—Žπ—‰z↔yx∈VβŸΌβ‹ƒxz
17 1 2 16 eqbrriv βŠ’π–‘π—‚π—€π–Όπ—Žπ—‰=x∈VβŸΌβ‹ƒx