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