Metamath Proof Explorer

Theorem eldmg

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

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

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = A -> ( x B y <-> A B y ) )
2 1 exbidv 
 |-  ( x = A -> ( E. y x B y <-> E. y A B y ) )
3 df-dm 
 |-  dom B = { x | E. y x B y }
4 2 3 elab2g 
 |-  ( A e. V -> ( A e. dom B <-> E. y A B y ) )