Metamath Proof Explorer


Theorem fnpm

Description: Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion fnpm
|- ^pm Fn ( _V X. _V )

Proof

Step Hyp Ref Expression
1 df-pm
 |-  ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
2 vex
 |-  y e. _V
3 vex
 |-  x e. _V
4 2 3 xpex
 |-  ( y X. x ) e. _V
5 4 pwex
 |-  ~P ( y X. x ) e. _V
6 5 rabex
 |-  { f e. ~P ( y X. x ) | Fun f } e. _V
7 1 6 fnmpoi
 |-  ^pm Fn ( _V X. _V )