Metamath Proof Explorer

Theorem nfvres

Description: The value of a non-member of a restriction is the empty set. (An artifact of our function value definition.) (Contributed by NM, 13-Nov-1995)

Ref Expression
Assertion nfvres ¬ A B F B A =


Step Hyp Ref Expression
1 dmres dom F B = B dom F
2 inss1 B dom F B
3 1 2 eqsstri dom F B B
4 3 sseli A dom F B A B
5 ndmfv ¬ A dom F B F B A =
6 4 5 nsyl5 ¬ A B F B A =