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 ⊢ A ∈ V
Assertion fvresex ⊢ y | ∃ x y = F ↾ A ⁡ x ∈ V

Proof

Step Hyp Ref Expression
1 fvresex.1 ⊢ A ∈ V
2 ssv ⊢ A ⊆ V
3 resmpt ⊢ A ⊆ V → z ∈ V ⟼ F ⁡ z ↾ A = z ∈ A ⟼ F ⁡ z
4 2 3 ax-mp ⊢ z ∈ V ⟼ F ⁡ z ↾ A = z ∈ A ⟼ F ⁡ z
5 4 fveq1i ⊢ z ∈ V ⟼ F ⁡ z ↾ A ⁡ x = z ∈ A ⟼ F ⁡ z ⁡ x
6 fveq2 ⊢ z = x → F ⁡ z = F ⁡ x
7 eqid ⊢ z ∈ V ⟼ F ⁡ z = z ∈ V ⟼ F ⁡ z
8 fvex ⊢ F ⁡ x ∈ V
9 6 7 8 fvmpt ⊢ x ∈ V → z ∈ V ⟼ F ⁡ z ⁡ x = F ⁡ x
10 9 elv ⊢ z ∈ V ⟼ F ⁡ z ⁡ x = F ⁡ x
11 fveqres ⊢ z ∈ V ⟼ F ⁡ z ⁡ x = F ⁡ x → z ∈ V ⟼ F ⁡ z ↾ A ⁡ x = F ↾ A ⁡ x
12 10 11 ax-mp ⊢ z ∈ V ⟼ F ⁡ z ↾ A ⁡ x = F ↾ A ⁡ x
13 5 12 eqtr3i ⊢ z ∈ A ⟼ F ⁡ z ⁡ x = F ↾ A ⁡ x
14 13 eqeq2i ⊢ y = z ∈ A ⟼ F ⁡ z ⁡ x ↔ y = F ↾ A ⁡ x
15 14 exbii ⊢ ∃ x y = z ∈ A ⟼ F ⁡ z ⁡ x ↔ ∃ x y = F ↾ A ⁡ x
16 15 abbii ⊢ y | ∃ x y = z ∈ A ⟼ F ⁡ z ⁡ x = y | ∃ x y = F ↾ A ⁡ x
17 1 mptex ⊢ z ∈ A ⟼ F ⁡ z ∈ V
18 17 fvclex ⊢ y | ∃ x y = z ∈ A ⟼ F ⁡ z ⁡ x ∈ V
19 16 18 eqeltrri ⊢ y | ∃ x y = F ↾ A ⁡ x ∈ V