f:(A inj
B), a:A. f 
{x:A| 
x = a } inj {y:B| y = f(a) }f:(A inj B), a:A. f {x:A| x = a }
{y:B| y = f(a) }| Theorem | Name |
| f:(A inj B), a:A. f {x:A| x = a } inj {y:B| y = f(a) } | [inj_point_deletion_inj] |
| cites the following: | |
| f:(A inj B), a:A. f {x:A| x = a }{y:B| y = f(a) } | [inj_point_deletion] |