Theorem afv2eu

Description: The value of a function at a unique point, analogous to fveu . (Contributed by AV, 5-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		eubrv	|- ( E! x A F x -> A e. _V )
2		euex	|- ( E! x A F x -> E. x A F x )
3		eldmg	|- ( A e. _V -> ( A e. dom F <-> E. x A F x ) )
4	2 3	syl5ibrcom	|- ( E! x A F x -> ( A e. _V -> A e. dom F ) )
5	4	impcom	|- ( ( A e. _V /\ E! x A F x ) -> A e. dom F )
6		dfdfat2	|- ( F defAt A <-> ( A e. dom F /\ E! x A F x ) )
7		dfatafv2iota	|- ( F defAt A -> ( F '''' A ) = ( iota x A F x ) )
8		iotauni	|- ( E! x A F x -> ( iota x A F x ) = U. { x | A F x } )
9	7 8	sylan9eq	|- ( ( F defAt A /\ E! x A F x ) -> ( F '''' A ) = U. { x | A F x } )
10	9	ex	|- ( F defAt A -> ( E! x A F x -> ( F '''' A ) = U. { x | A F x } ) )
11	6 10	sylbir	|- ( ( A e. dom F /\ E! x A F x ) -> ( E! x A F x -> ( F '''' A ) = U. { x | A F x } ) )
12	11	expcom	|- ( E! x A F x -> ( A e. dom F -> ( E! x A F x -> ( F '''' A ) = U. { x | A F x } ) ) )
13	12	pm2.43a	|- ( E! x A F x -> ( A e. dom F -> ( F '''' A ) = U. { x | A F x } ) )
14	13	adantl	|- ( ( A e. _V /\ E! x A F x ) -> ( A e. dom F -> ( F '''' A ) = U. { x | A F x } ) )
15	5 14	mpd	|- ( ( A e. _V /\ E! x A F x ) -> ( F '''' A ) = U. { x | A F x } )
16	1 15	mpancom	|- ( E! x A F x -> ( F '''' A ) = U. { x | A F x } )