Metamath Proof Explorer

Theorem dfbigcup2

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

Ref Expression
Assertion dfbigcup2 
|- Bigcup = ( x e. _V |-> U. x )

Proof

Step Hyp Ref Expression
1 relbigcup 
 |-  Rel Bigcup
2 mptrel 
 |-  Rel ( x e. _V |-> U. x )
3 eqcom 
 |-  ( U. y = z <-> z = U. y )
4 vex 
 |-  z e. _V
5 4 brbigcup 
 |-  ( y Bigcup z <-> U. y = z )
6 vex 
 |-  y e. _V
7 eleq1w 
 |-  ( x = y -> ( x e. _V <-> y e. _V ) )
8 unieq 
 |-  ( x = y -> U. x = U. y )
9 8 eqeq2d 
 |-  ( x = y -> ( t = U. x <-> t = U. y ) )
10 7 9 anbi12d 
 |-  ( x = y -> ( ( x e. _V /\ t = U. x ) <-> ( y e. _V /\ t = U. y ) ) )
11 6 biantrur 
 |-  ( t = U. y <-> ( y e. _V /\ t = U. y ) )
12 10 11 bitr4di 
 |-  ( x = y -> ( ( x e. _V /\ t = U. x ) <-> t = U. y ) )
13 eqeq1 
 |-  ( t = z -> ( t = U. y <-> z = U. y ) )
14 df-mpt 
 |-  ( x e. _V |-> U. x ) = { <. x , t >. | ( x e. _V /\ t = U. x ) }
15 6 4 12 13 14 brab 
 |-  ( y ( x e. _V |-> U. x ) z <-> z = U. y )
16 3 5 15 3bitr4i 
 |-  ( y Bigcup z <-> y ( x e. _V |-> U. x ) z )
17 1 2 16 eqbrriv 
 |-  Bigcup = ( x e. _V |-> U. x )