Metamath Proof Explorer

Theorem abrexdom2jm

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

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

Proof

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