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

Metamath Proof Explorer

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 ) )