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

Metamath Proof Explorer

Theorem fsetex

Description: The set of functions between two classes exists if the codomain exists. Generalization of mapex to arbitrary domains. (Contributed by AV, 14-Aug-2024)

Ref Expression
Assertion fsetex ⊢ B ∈ V → f | f : A ⟶ B ∈ V

Proof

Step Hyp Ref Expression
1 mapfset ⊢ B ∈ V → f | f : A ⟶ B = B A
2 ovex ⊢ B A ∈ V
3 1 2 eqeltrdi ⊢ B ∈ V → f | f : A ⟶ B ∈ V