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 NM, 22-Apr-2005) (Revised by Mario Carneiro, 20-Dec-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mptex.1 | |- A e. _V |
|
| Assertion | mptex | |- ( x e. A |-> B ) e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mptex.1 | |- A e. _V |
|
| 2 | mptexg | |- ( A e. _V -> ( x e. A |-> B ) e. _V ) |
|
| 3 | 1 2 | ax-mp | |- ( x e. A |-> B ) e. _V |