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 ⊢ A ∈ V → x | ∃ y ∈ A x = B ≼ A

Proof

Step Hyp Ref Expression
1 moeq ⊢ ∃* x x = B
2 1 a1i ⊢ y ∈ A → ∃* x x = B
3 2 abrexdomjm ⊢ A ∈ V → x | ∃ y ∈ A x = B ≼ A