Theorem abrexexd

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

	Ref	Expression
Hypotheses	abrexexd.0	⊢ Ⅎ 𝑥 𝐴
	abrexexd.1	⊢ ( 𝜑 → 𝐴 ∈ V )
Assertion	abrexexd	⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		abrexexd.0	⊢ Ⅎ 𝑥 𝐴
2		abrexexd.1	⊢ ( 𝜑 → 𝐴 ∈ V )
3		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
4		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
5	4	rneqi	⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
6		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
7	6	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
8	3 5 7	3eqtr4i	⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
9		funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
11	10	dmmpt	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
12	1	rabexgfGS	⊢ ( 𝐴 ∈ V → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ∈ V )
13	11 12	eqeltrid	⊢ ( 𝐴 ∈ V → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
14		funex	⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
15	9 13 14	sylancr	⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
16		rnexg	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
17	2 15 16	3syl	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
18	8 17	eqeltrrid	⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )