Metamath Proof Explorer


Theorem mptexf

Description: If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses mptexf.1
|- F/_ x A
mptexf.2
|- A e. _V
Assertion mptexf
|- ( x e. A |-> B ) e. _V

Proof

Step Hyp Ref Expression
1 mptexf.1
 |-  F/_ x A
2 mptexf.2
 |-  A e. _V
3 1 mptexgf
 |-  ( A e. _V -> ( x e. A |-> B ) e. _V )
4 2 3 ax-mp
 |-  ( x e. A |-> B ) e. _V