Metamath Proof Explorer

Theorem fnmap

Description: Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion fnmap 
|- ^m Fn ( _V X. _V )

Proof

Step Hyp Ref Expression
1 df-map 
 |-  ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
2 mapex 
 |-  ( ( y e. _V /\ x e. _V ) -> { f | f : y --> x } e. _V )
3 2 el2v 
 |-  { f | f : y --> x } e. _V
4 1 3 fnmpoi 
 |-  ^m Fn ( _V X. _V )