Metamath Proof Explorer

Theorem afvprc

Description: A function's value at a proper class is the universe, compare with fvprc . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afvprc 
|- ( -. A e. _V -> ( F ''' A ) = _V )

Proof

Step Hyp Ref Expression
1 prcnel 
 |-  ( -. A e. _V -> -. A e. dom F )
2 ndmafv 
 |-  ( -. A e. dom F -> ( F ''' A ) = _V )
3 1 2 syl 
 |-  ( -. A e. _V -> ( F ''' A ) = _V )