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 = w -> ( x B y <-> w B y ) )
2 1 exbidv 
 |-  ( x = w -> ( E. y x B y <-> E. y w B y ) )
3 breq1 
 |-  ( w = A -> ( w B y <-> A B y ) )
4 3 exbidv 
 |-  ( w = A -> ( E. y w B y <-> E. y A B y ) )
5 df-dm 
 |-  dom B = { x | E. y x B y }
6 2 4 5 elab2gw 
 |-  ( A e. V -> ( A e. dom B <-> E. y A B y ) )