Theorem abrexdom2

Description: An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		moeq	⊢ ∃* 𝑥 𝑥 = 𝐵
2	1	a1i	⊢ ( 𝑦 ∈ 𝐴 → ∃* 𝑥 𝑥 = 𝐵 )
3	2	abrexdom	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } ≼ 𝐴 )