Description: If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn . (Contributed by Alexander van der Vekens, 25-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfunsnafv | |- ( -. Fun ( F |` { A } ) -> ( F ''' A ) = _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-dfat | |- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) ) |
|
| 2 | 1 | simprbi | |- ( F defAt A -> Fun ( F |` { A } ) ) |
| 3 | afvnfundmuv | |- ( -. F defAt A -> ( F ''' A ) = _V ) |
|
| 4 | 2 3 | nsyl5 | |- ( -. Fun ( F |` { A } ) -> ( F ''' A ) = _V ) |