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 AVx|yAx=BA

Proof

Step Hyp Ref Expression
1 moeq *xx=B
2 1 a1i yA*xx=B
3 2 abrexdomjm AVx|yAx=BA