This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = (/) )