Metamath Proof Explorer

Theorem abrexct

Description: An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
2 1 rnmpt 
 |-  ran ( x e. A |-> B ) = { y | E. x e. A y = B }
3 1stcrestlem 
 |-  ( A ~<_ _om -> ran ( x e. A |-> B ) ~<_ _om )
4 2 3 eqbrtrrid 
 |-  ( A ~<_ _om -> { y | E. x e. A y = B } ~<_ _om )