Metamath Proof Explorer


Theorem abrexdom2

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

Ref Expression
Assertion abrexdom2
|- ( A e. V -> { x | E. y e. A x = B } ~<_ A )

Proof

Step Hyp Ref Expression
1 moeq
 |-  E* x x = B
2 1 a1i
 |-  ( y e. A -> E* x x = B )
3 2 abrexdom
 |-  ( A e. V -> { x | E. y e. A x = B } ~<_ A )