Metamath Proof Explorer

Theorem ndmafv

Description: The value of a class outside its domain is the universe, compare with ndmfv . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Proof

Step Hyp Ref Expression
1 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
2 1 simplbi 
 |-  ( F defAt A -> A e. dom F )
3 afvnfundmuv 
 |-  ( -. F defAt A -> ( F ''' A ) = _V )
4 2 3 nsyl5 
 |-  ( -. A e. dom F -> ( F ''' A ) = _V )