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

Metamath Proof Explorer

Theorem dmopab

Description: The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 4-Dec-2016)

Ref Expression
Assertion dmopab 
|- dom { <. x , y >. | ph } = { x | E. y ph }

Proof

Step Hyp Ref Expression
1 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
2 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
3 1 2 dfdmf 
 |-  dom { <. x , y >. | ph } = { x | E. y x { <. x , y >. | ph } y }
4 df-br 
 |-  ( x { <. x , y >. | ph } y <-> <. x , y >. e. { <. x , y >. | ph } )
5 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
6 4 5 bitri 
 |-  ( x { <. x , y >. | ph } y <-> ph )
7 6 exbii 
 |-  ( E. y x { <. x , y >. | ph } y <-> E. y ph )
8 7 abbii 
 |-  { x | E. y x { <. x , y >. | ph } y } = { x | E. y ph }
9 3 8 eqtri 
 |-  dom { <. x , y >. | ph } = { x | E. y ph }