This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )