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	|- F/_ x A
Assertion	abrexctf	|- ( A ~<_ _om -> { y | E. x e. A y = B } ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		mptctf.1	|- F/_ x A
2		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
3	2	rnmpt	|- ran ( x e. A |-> B ) = { y | E. x e. A y = B }
4	1	mptctf	|- ( A ~<_ _om -> ( x e. A |-> B ) ~<_ _om )
5		rnct	|- ( ( x e. A |-> B ) ~<_ _om -> ran ( x e. A |-> B ) ~<_ _om )
6	4 5	syl	|- ( A ~<_ _om -> ran ( x e. A |-> B ) ~<_ _om )
7	3 6	eqbrtrrid	|- ( A ~<_ _om -> { y | E. x e. A y = B } ~<_ _om )