# Metamath Proof Explorer

## Theorem fnex

Description: If the domain of a function is a set, the function is a set. Theorem 6.16(1) of TakeutiZaring p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg . See fnexALT for alternate proof. (Contributed by NM, 14-Aug-1994) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fnex ${⊢}\left({F}Fn{A}\wedge {A}\in {B}\right)\to {F}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 fnrel ${⊢}{F}Fn{A}\to \mathrm{Rel}{F}$
2 df-fn ${⊢}{F}Fn{A}↔\left(\mathrm{Fun}{F}\wedge \mathrm{dom}{F}={A}\right)$
3 eleq1a ${⊢}{A}\in {B}\to \left(\mathrm{dom}{F}={A}\to \mathrm{dom}{F}\in {B}\right)$
4 3 impcom ${⊢}\left(\mathrm{dom}{F}={A}\wedge {A}\in {B}\right)\to \mathrm{dom}{F}\in {B}$
5 resfunexg ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{dom}{F}\in {B}\right)\to {{F}↾}_{\mathrm{dom}{F}}\in \mathrm{V}$
6 4 5 sylan2 ${⊢}\left(\mathrm{Fun}{F}\wedge \left(\mathrm{dom}{F}={A}\wedge {A}\in {B}\right)\right)\to {{F}↾}_{\mathrm{dom}{F}}\in \mathrm{V}$
7 6 anassrs ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{dom}{F}={A}\right)\wedge {A}\in {B}\right)\to {{F}↾}_{\mathrm{dom}{F}}\in \mathrm{V}$
8 2 7 sylanb ${⊢}\left({F}Fn{A}\wedge {A}\in {B}\right)\to {{F}↾}_{\mathrm{dom}{F}}\in \mathrm{V}$
9 resdm ${⊢}\mathrm{Rel}{F}\to {{F}↾}_{\mathrm{dom}{F}}={F}$
10 9 eleq1d ${⊢}\mathrm{Rel}{F}\to \left({{F}↾}_{\mathrm{dom}{F}}\in \mathrm{V}↔{F}\in \mathrm{V}\right)$
11 10 biimpa ${⊢}\left(\mathrm{Rel}{F}\wedge {{F}↾}_{\mathrm{dom}{F}}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
12 1 8 11 syl2an2r ${⊢}\left({F}Fn{A}\wedge {A}\in {B}\right)\to {F}\in \mathrm{V}$