This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid 
 |-  ( 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 eqtrid 
 |-  ( R = { <. x , y >. | ph } -> dom R = { x | E. y ph } )