Theorem afveu

Description: The value of a function at a unique point, analogous to fveu . (Contributed by Alexander van der Vekens, 29-Nov-2017)

	Ref	Expression
Assertion	afveu	|- ( E! x A F x -> ( F ''' A ) = U. { x | A F x } )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( A F x <-> <. A , x >. e. F )
2	1	eubii	|- ( E! x A F x <-> E! x <. A , x >. e. F )
3		eu2ndop1stv	|- ( E! x <. A , x >. e. F -> A e. _V )
4	2 3	sylbi	|- ( E! x A F x -> A e. _V )
5		euex	|- ( E! x A F x -> E. x A F x )
6		eldmg	|- ( A e. _V -> ( A e. dom F <-> E. x A F x ) )
7	5 6	syl5ibrcom	|- ( E! x A F x -> ( A e. _V -> A e. dom F ) )
8	7	impcom	|- ( ( A e. _V /\ E! x A F x ) -> A e. dom F )
9		dfdfat2	|- ( F defAt A <-> ( A e. dom F /\ E! x A F x ) )
10		afvfundmfveq	|- ( F defAt A -> ( F ''' A ) = ( F ` A ) )
11		fveu	|- ( E! x A F x -> ( F ` A ) = U. { x | A F x } )
12	10 11	sylan9eq	|- ( ( F defAt A /\ E! x A F x ) -> ( F ''' A ) = U. { x | A F x } )
13	12	ex	|- ( F defAt A -> ( E! x A F x -> ( F ''' A ) = U. { x | A F x } ) )
14	9 13	sylbir	|- ( ( A e. dom F /\ E! x A F x ) -> ( E! x A F x -> ( F ''' A ) = U. { x | A F x } ) )
15	14	expcom	|- ( E! x A F x -> ( A e. dom F -> ( E! x A F x -> ( F ''' A ) = U. { x | A F x } ) ) )
16	15	pm2.43a	|- ( E! x A F x -> ( A e. dom F -> ( F ''' A ) = U. { x | A F x } ) )
17	16	adantl	|- ( ( A e. _V /\ E! x A F x ) -> ( A e. dom F -> ( F ''' A ) = U. { x | A F x } ) )
18	8 17	mpd	|- ( ( A e. _V /\ E! x A F x ) -> ( F ''' A ) = U. { x | A F x } )
19	4 18	mpancom	|- ( E! x A F x -> ( F ''' A ) = U. { x | A F x } )