Theorem abrexct

Description: An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016) (Moved to the main part of set.mm by Vincent Gonzalez, 19-Aug-2026.)

	Ref	Expression
Assertion	abrexct	$$⊢A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists x\in Ay=B\right\}\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
2	1	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\left\{y|\exists x\in Ay=B\right\}$$
3		1stcrestlem	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{ran}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
4	2 3	eqbrtrrid	$$⊢A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists x\in Ay=B\right\}\preccurlyeq \mathrm{\omega }$$