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 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 abrexdomjm 
 |-  ( A e. V -> { x | E. y e. A x = B } ~<_ A )