Theorem opabrn

Description: Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017)

	Ref	Expression
Assertion	opabrn	|- ( R = { <. x , y >. | ph } -> ran R = { y | E. x ph } )

Proof

Step	Hyp	Ref	Expression
1		dfrn2	|- ran R = { y | E. x x R y }
2		nfopab2	|- F/_ y { <. x , y >. | ph }
3	2	nfeq2	|- F/ y R = { <. x , y >. | ph }
4		nfopab1	|- F/_ x { <. x , y >. | ph }
5	4	nfeq2	|- F/ x R = { <. x , y >. | ph }
6		df-br	|- ( x R y <-> <. x , y >. e. R )
7		eleq2	|- ( R = { <. x , y >. | ph } -> ( <. x , y >. e. R <-> <. x , y >. e. { <. x , y >. | ph } ) )
8		opabidw	|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
9	7 8	bitrdi	|- ( R = { <. x , y >. | ph } -> ( <. x , y >. e. R <-> ph ) )
10	6 9	bitrid	|- ( R = { <. x , y >. | ph } -> ( x R y <-> ph ) )
11	5 10	exbid	|- ( R = { <. x , y >. | ph } -> ( E. x x R y <-> E. x ph ) )
12	3 11	abbid	|- ( R = { <. x , y >. | ph } -> { y | E. x x R y } = { y | E. x ph } )
13	1 12	eqtrid	|- ( R = { <. x , y >. | ph } -> ran R = { y | E. x ph } )