# 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
`|- ( ( F Fn A /\ A e. B ) -> F e. _V )`

### Proof

Step Hyp Ref Expression
1 fnrel
` |-  ( F Fn A -> Rel F )`
2 df-fn
` |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )`
3 eleq1a
` |-  ( A e. B -> ( dom F = A -> dom F e. B ) )`
4 3 impcom
` |-  ( ( dom F = A /\ A e. B ) -> dom F e. B )`
5 resfunexg
` |-  ( ( Fun F /\ dom F e. B ) -> ( F |` dom F ) e. _V )`
6 4 5 sylan2
` |-  ( ( Fun F /\ ( dom F = A /\ A e. B ) ) -> ( F |` dom F ) e. _V )`
7 6 anassrs
` |-  ( ( ( Fun F /\ dom F = A ) /\ A e. B ) -> ( F |` dom F ) e. _V )`
8 2 7 sylanb
` |-  ( ( F Fn A /\ A e. B ) -> ( F |` dom F ) e. _V )`
9 resdm
` |-  ( Rel F -> ( F |` dom F ) = F )`
10 9 eleq1d
` |-  ( Rel F -> ( ( F |` dom F ) e. _V <-> F e. _V ) )`
11 10 biimpa
` |-  ( ( Rel F /\ ( F |` dom F ) e. _V ) -> F e. _V )`
12 1 8 11 syl2an2r
` |-  ( ( F Fn A /\ A e. B ) -> F e. _V )`