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 )