Metamath Proof Explorer

Theorem dfdm3

Description: Alternate definition of domain. Definition 6.5(1) of TakeutiZaring p. 24. (Contributed by NM, 28-Dec-1996)

Ref Expression
Assertion dfdm3 
|- dom A = { x | E. y <. x , y >. e. A }

Proof

Step Hyp Ref Expression
1 df-dm 
 |-  dom A = { x | E. y x A y }
2 df-br 
 |-  ( x A y <-> <. x , y >. e. A )
3 2 exbii 
 |-  ( E. y x A y <-> E. y <. x , y >. e. A )
4 3 abbii 
 |-  { x | E. y x A y } = { x | E. y <. x , y >. e. A }
5 1 4 eqtri 
 |-  dom A = { x | E. y <. x , y >. e. A }