Metamath Proof Explorer

Theorem eldm2g

Description: Domain membership. Theorem 4 of Suppes p. 59. (Contributed by NM, 27-Jan-1997) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Assertion eldm2g 
|- ( A e. V -> ( A e. dom B <-> E. y <. A , y >. e. B ) )

Proof

Step Hyp Ref Expression
1 eldmg 
 |-  ( A e. V -> ( A e. dom B <-> E. y A B y ) )
2 df-br 
 |-  ( A B y <-> <. A , y >. e. B )
3 2 exbii 
 |-  ( E. y A B y <-> E. y <. A , y >. e. B )
4 1 3 bitrdi 
 |-  ( A e. V -> ( A e. dom B <-> E. y <. A , y >. e. B ) )