Theorem opabdm

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

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

Proof

Step	Hyp	Ref	Expression
1		df-dm	|- dom R = { x | E. y x R y }
2		nfopab1	|- F/_ x { <. x , y >. | ph }
3	2	nfeq2	|- F/ x R = { <. x , y >. | ph }
4		nfopab2	|- F/_ y { <. x , y >. | ph }
5	4	nfeq2	|- F/ y 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	syl5bb	|- ( R = { <. x , y >. | ph } -> ( x R y <-> ph ) )
11	5 10	exbid	|- ( R = { <. x , y >. | ph } -> ( E. y x R y <-> E. y ph ) )
12	3 11	abbid	|- ( R = { <. x , y >. | ph } -> { x | E. y x R y } = { x | E. y ph } )
13	1 12	syl5eq	|- ( R = { <. x , y >. | ph } -> dom R = { x | E. y ph } )