Metamath Proof Explorer

Theorem abrexexd

Description: Existence of a class abstraction of existentially restricted sets. (Contributed by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses abrexexd.0 ⊢ Ⅎ _ x A
abrexexd.1 ⊢ φ → A ∈ V
Assertion abrexexd ⊢ φ → y | ∃ x ∈ A y = B ∈ V

Proof

Step Hyp Ref Expression
1 abrexexd.0 ⊢ Ⅎ _ x A
2 abrexexd.1 ⊢ φ → A ∈ V
3 rnopab ⊢ ran ⁡ x y | x ∈ A ∧ y = B = y | ∃ x x ∈ A ∧ y = B
4 df-mpt ⊢ x ∈ A ⟼ B = x y | x ∈ A ∧ y = B
5 4 rneqi ⊢ ran ⁡ x ∈ A ⟼ B = ran ⁡ x y | x ∈ A ∧ y = B
6 df-rex ⊢ ∃ x ∈ A y = B ↔ ∃ x x ∈ A ∧ y = B
7 6 abbii ⊢ y | ∃ x ∈ A y = B = y | ∃ x x ∈ A ∧ y = B
8 3 5 7 3eqtr4i ⊢ ran ⁡ x ∈ A ⟼ B = y | ∃ x ∈ A y = B
9 funmpt ⊢ Fun ⁡ x ∈ A ⟼ B
10 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
11 10 dmmpt ⊢ dom ⁡ x ∈ A ⟼ B = x ∈ A | B ∈ V
12 1 rabexgfGS ⊢ A ∈ V → x ∈ A | B ∈ V ∈ V
13 11 12 eqeltrid ⊢ A ∈ V → dom ⁡ x ∈ A ⟼ B ∈ V
14 funex ⊢ Fun ⁡ x ∈ A ⟼ B ∧ dom ⁡ x ∈ A ⟼ B ∈ V → x ∈ A ⟼ B ∈ V
15 9 13 14 sylancr ⊢ A ∈ V → x ∈ A ⟼ B ∈ V
16 rnexg ⊢ x ∈ A ⟼ B ∈ V → ran ⁡ x ∈ A ⟼ B ∈ V
17 2 15 16 3syl ⊢ φ → ran ⁡ x ∈ A ⟼ B ∈ V
18 8 17 eqeltrrid ⊢ φ → y | ∃ x ∈ A y = B ∈ V