Theorem afv2ex

Description: The alternate function value is always a set if the range of the function is a set. (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	afv2ex	|- ( ran F e. V -> ( F '''' A ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-afv2	|- ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F )
2		iotaex	|- ( iota x A F x ) e. _V
3	2	a1i	|- ( ran F e. V -> ( iota x A F x ) e. _V )
4		uniexg	|- ( ran F e. V -> U. ran F e. _V )
5	4	pwexd	|- ( ran F e. V -> ~P U. ran F e. _V )
6	3 5	ifcld	|- ( ran F e. V -> if ( F defAt A , ( iota x A F x ) , ~P U. ran F ) e. _V )
7	1 6	eqeltrid	|- ( ran F e. V -> ( F '''' A ) e. _V )