Theorem abrexexg

Description: Existence of a class abstraction of existentially restricted sets. The class B can be thought of as an expression in x (which is typically a free variable in the class expression substituted for B ) and the class abstraction appearing in the statement as the class of values B as x varies through A . If the "domain" A is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path mptexg , funex , fnex , resfunexg , and funimaexg . See also abrexex2g . There are partial converses under additional conditions, see for instance abnexg . (Contributed by NM, 3-Nov-2003) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	abrexexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	rnmpt	⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
3		mptexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
4		rnexg	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
5	3 4	syl	⊢ ( 𝐴 ∈ 𝑉 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
6	2 5	eqeltrrid	⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )