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

Metamath Proof Explorer

Theorem fvresex

Description: Existence of the class of values of a restricted class. (Contributed by NM, 14-Nov-1995) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis fvresex.1 ⊢ 𝐴 ∈ V
Assertion fvresex { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) } ∈ V

Proof

Step Hyp Ref Expression
1 fvresex.1 ⊢ 𝐴 ∈ V
2 ssv ⊢ 𝐴 ⊆ V
3 resmpt ⊢ ( 𝐴 ⊆ V → ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
4 2 3 ax-mp ⊢ ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) )
5 4 fveq1i ⊢ ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 )
6 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
7 eqid ⊢ ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) )
8 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
9 6 7 8 fvmpt ⊢ ( 𝑥 ∈ V → ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
10 9 elv ⊢ ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
11 fveqres ⊢ ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
12 10 11 ax-mp ⊢ ( ( ( 𝑧 ∈ V ↦ ( 𝐹 ‘ 𝑧 ) ) ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 )
13 5 12 eqtr3i ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 )
14 13 eqeq2i ⊢ ( 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
15 14 exbii ⊢ ( ∃ 𝑥 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) ↔ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
16 15 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) }
17 1 mptex ⊢ ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ V
18 17 fvclex ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) ‘ 𝑥 ) } ∈ V
19 16 18 eqeltrri ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) } ∈ V