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 ( ( 𝐹 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 )