Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bigcup Structured version   Unicode version

Definition df-bigcup 25702
Description: Define the Bigcup function, which, per fvbigcup 25747, carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012.)
Assertion
Ref Expression
df-bigcup  |-  Bigcup  =  ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) ( (  _E  o.  _E  )  (x)  _V )
) )

Detailed syntax breakdown of Definition df-bigcup
StepHypRef Expression
1 cbigcup 25678 . 2  class  Bigcup
2 cvv 2956 . . . 4  class  _V
32, 2cxp 4876 . . 3  class  ( _V 
X.  _V )
4 cep 4492 . . . . . 6  class  _E
52, 4ctxp 25674 . . . . 5  class  ( _V 
(x)  _E  )
64, 4ccom 4882 . . . . . 6  class  (  _E  o.  _E  )
76, 2ctxp 25674 . . . . 5  class  ( (  _E  o.  _E  )  (x)  _V )
85, 7csymdif 25662 . . . 4  class  ( ( _V  (x)  _E  )(++) ( (  _E  o.  _E  )  (x)  _V )
)
98crn 4879 . . 3  class  ran  (
( _V  (x)  _E  )(++) ( (  _E  o.  _E  )  (x)  _V )
)
103, 9cdif 3317 . 2  class  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )(++) (
(  _E  o.  _E  )  (x)  _V ) ) )
111, 10wceq 1652 1  wff  Bigcup  =  ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) ( (  _E  o.  _E  )  (x)  _V )
) )
Colors of variables: wff set class
This definition is referenced by:  relbigcup  25742  brbigcup  25743
  Copyright terms: Public domain W3C validator