Metamath Proof Explorer


Theorem ndmafv2nrn

Description: The value of a class outside its domain is not in the range, compare with ndmfv . (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion ndmafv2nrn
|- ( -. A e. dom F -> ( F '''' A ) e/ ran F )

Proof

Step Hyp Ref Expression
1 orc
 |-  ( -. A e. dom F -> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) )
2 ianor
 |-  ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) <-> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) )
3 df-dfat
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
4 2 3 xchnxbir
 |-  ( -. F defAt A <-> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) )
5 1 4 sylibr
 |-  ( -. A e. dom F -> -. F defAt A )
6 ndfatafv2nrn
 |-  ( -. F defAt A -> ( F '''' A ) e/ ran F )
7 5 6 syl
 |-  ( -. A e. dom F -> ( F '''' A ) e/ ran F )