Metamath Proof Explorer

Theorem fnbigcup

Description: Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012)

Ref Expression
Assertion fnbigcup 
|- Bigcup Fn _V

Proof

Step Hyp Ref Expression
1 fobigcup 
 |-  Bigcup : _V -onto-> _V
2 fofn 
 |-  ( Bigcup : _V -onto-> _V -> Bigcup Fn _V )
3 1 2 ax-mp 
 |-  Bigcup Fn _V