Metamath Proof Explorer

Theorem fexd

Description: If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fexd.1 φ F : A B
fexd.2 φ A C
Assertion fexd φ F V


Step Hyp Ref Expression
1 fexd.1 φ F : A B
2 fexd.2 φ A C
3 fex F : A B A C F V
4 1 2 3 syl2anc φ F V