Theorem fsetcdmex

Description: The class of all functions from a nonempty set A into a class B is a set iff B is a set . (Contributed by AV, 15-Sep-2024)

	Ref	Expression
Assertion	fsetcdmex	|- ( ( A e. V /\ A =/= (/) ) -> ( B e. _V <-> { f | f : A --> B } e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		fsetex	|- ( B e. _V -> { f | f : A --> B } e. _V )
2		fsetprcnex	|- ( ( ( A e. V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )
3	2	ex	|- ( ( A e. V /\ A =/= (/) ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
4		df-nel	|- ( B e/ _V <-> -. B e. _V )
5		df-nel	|- ( { f | f : A --> B } e/ _V <-> -. { f | f : A --> B } e. _V )
6	3 4 5	3imtr3g	|- ( ( A e. V /\ A =/= (/) ) -> ( -. B e. _V -> -. { f | f : A --> B } e. _V ) )
7	6	con4d	|- ( ( A e. V /\ A =/= (/) ) -> ( { f | f : A --> B } e. _V -> B e. _V ) )
8	1 7	impbid2	|- ( ( A e. V /\ A =/= (/) ) -> ( B e. _V <-> { f | f : A --> B } e. _V ) )