# 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 ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → 𝐹 ∈ V )

### Proof

Step Hyp Ref Expression
1 fnrel ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2 df-fn ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
3 eleq1a ( 𝐴𝐵 → ( dom 𝐹 = 𝐴 → dom 𝐹𝐵 ) )
4 3 impcom ( ( dom 𝐹 = 𝐴𝐴𝐵 ) → dom 𝐹𝐵 )
5 resfunexg ( ( Fun 𝐹 ∧ dom 𝐹𝐵 ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
6 4 5 sylan2 ( ( Fun 𝐹 ∧ ( dom 𝐹 = 𝐴𝐴𝐵 ) ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
7 6 anassrs ( ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ∧ 𝐴𝐵 ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
8 2 7 sylanb ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → ( 𝐹 ↾ dom 𝐹 ) ∈ V )
9 resdm ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
10 9 eleq1d ( Rel 𝐹 → ( ( 𝐹 ↾ dom 𝐹 ) ∈ V ↔ 𝐹 ∈ V ) )
11 10 biimpa ( ( Rel 𝐹 ∧ ( 𝐹 ↾ dom 𝐹 ) ∈ V ) → 𝐹 ∈ V )
12 1 8 11 syl2an2r ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → 𝐹 ∈ V )