Theorem tz6.12-2

Description: Function value when F is not a function. Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by NM, 30-Apr-2004) (Proof shortened by Mario Carneiro, 31-Aug-2015) Avoid ax-10 , ax-11 , ax-12 . (Revised by TM, 25-Jan-2026)

	Ref	Expression
Assertion	tz6.12-2	|- ( -. E! x A F x -> ( F ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-fv	|- ( F ` A ) = ( iota y A F y )
2		eu6im	|- ( E. z A. x ( A F x <-> x = z ) -> E! x A F x )
3		breq2	|- ( y = x -> ( A F y <-> A F x ) )
4	3	eqabcbw	|- ( { y | A F y } = { z } <-> A. x ( A F x <-> x e. { z } ) )
5		velsn	|- ( x e. { z } <-> x = z )
6	5	bibi2i	|- ( ( A F x <-> x e. { z } ) <-> ( A F x <-> x = z ) )
7	6	albii	|- ( A. x ( A F x <-> x e. { z } ) <-> A. x ( A F x <-> x = z ) )
8	4 7	bitri	|- ( { y | A F y } = { z } <-> A. x ( A F x <-> x = z ) )
9	8	exbii	|- ( E. z { y | A F y } = { z } <-> E. z A. x ( A F x <-> x = z ) )
10		iotanul2	|- ( -. E. z { y | A F y } = { z } -> ( iota y A F y ) = (/) )
11	9 10	sylnbir	|- ( -. E. z A. x ( A F x <-> x = z ) -> ( iota y A F y ) = (/) )
12	2 11	nsyl5	|- ( -. E! x A F x -> ( iota y A F y ) = (/) )
13	1 12	eqtrid	|- ( -. E! x A F x -> ( F ` A ) = (/) )