Theorem abrexctf

Description: An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypothesis	mptctf.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	abrexctf	$$⊢A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists x\in Ay=B\right\}\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		mptctf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
3	2	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\left\{y|\exists x\in Ay=B\right\}$$
4	1	mptctf	$$⊢A\preccurlyeq \mathrm{\omega }\to \left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
5		rnct	$$⊢\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }\to \mathrm{ran}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
6	4 5	syl	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{ran}\left(x\in A⟼B\right)\preccurlyeq \mathrm{\omega }$$
7	3 6	eqbrtrrid	$$⊢A\preccurlyeq \mathrm{\omega }\to \left\{y|\exists x\in Ay=B\right\}\preccurlyeq \mathrm{\omega }$$